<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
<link href="common/css/sf.css" rel="stylesheet" type="text/css"/>
<title>Poly: 多态与高阶函数</title>
</head>
<link href="common/jquery-ui/jquery-ui.css" rel="stylesheet">
<script src="common/jquery-ui/external/jquery/jquery.js"></script>
<script src="common/jquery-ui/jquery-ui.js"></script>
<script src="common/toggleproofs.js"></script>
<link href="common/css/lf.css" rel="stylesheet" type="text/css"/>

<body>

<div id="page">

<div id="header">
<a href='https://coq-zh.github.io/SF-zh/index.html'>
<img src='common/media/image/sf_logo_sm.png'></a>
</br><a href='index.html'>  <span class='booktitleinheader'>Volume 1: 逻辑基础</span><br></br>
<ul id='menu'>
   <a href='toc.html'><li class='section_name'>目录</li></a>
   <a href='coqindex.html'><li class='section_name'>索引</li></a>
   <a href='deps.html'><li class='section_name'>路线</li></a>
</ul>
</a></div>

<div id="main">

<h1 class="libtitle">Poly<span class="subtitle">多态与高阶函数</span></h1>


<div class="code code-tight">

<span class="comment">(*&nbsp;Suppress&nbsp;some&nbsp;annoying&nbsp;warnings&nbsp;from&nbsp;Coq:&nbsp;*)</span><br/>
<span class="id" type="keyword">Set</span> <span class="id" type="var">Warnings</span> "-notation-overridden,-parsing".<br/>
<span class="id" type="var">From</span> <span class="id" type="var">LF</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Export</span> <span class="id" type="var">Lists</span>.<br/>
</div>

<div class="doc">
<a name="lab101"></a><h1 class="section">多态</h1>

<div class="paragraph"> </div>

 在本章中，我们会继续发展函数式编程的基本概念，其中最关键的新概念就是
    <b>多态</b>（在所处理的数据类型上抽象出函数）和<b>高阶函数</b>（函数作为数据）。 
</div>

<div class="doc">
<a name="lab102"></a><h2 class="section">多态列表</h2>

<div class="paragraph"> </div>

 在前几章中，我们只是使用了数的列表。很明显，
    有趣的程序还需要能够处理其它元素类型的列表，如字符串列表、布尔值列表、
    列表的列表等等。我们<b>可以</b>分别为它们定义新的归纳数据类型，例如... 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">boollist</span> : <span class="id" type="keyword">Type</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">bool_nil</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">bool_cons</span> (<span class="id" type="var">b</span> : <span class="id" type="var">bool</span>) (<span class="id" type="var">l</span> : <span class="id" type="var">boollist</span>).<br/>
</div>

<div class="doc">
...不过这样很快就会变得乏味。
    部分原因在于我们必须为每种数据类型都定义不同的构造子，
    然而主因还是我们必须为每种数据类型再重新定义一遍所有的列表处理函数
    （如 <span class="inlinecode"><span class="id" type="var">length</span></span>、<span class="inlinecode"><span class="id" type="var">rev</span></span> 等）。 
<div class="paragraph"> </div>

 为避免这些重复，Coq 支持定义<b>多态</b>归纳类型。
    例如，以下就是<b>多态列表</b>数据类型。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">list</span> (<span class="id" type="var">X</span>:<span class="id" type="keyword">Type</span>) : <span class="id" type="keyword">Type</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">nil</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">cons</span> (<span class="id" type="var">x</span> : <span class="id" type="var">X</span>) (<span class="id" type="var">l</span> : <span class="id" type="var">list</span> <span class="id" type="var">X</span>).<br/>
</div>

<div class="doc">
这和上一章中 <span class="inlinecode"><span class="id" type="var">natlist</span></span> 的定义基本一样，只是将 <span class="inlinecode"><span class="id" type="var">cons</span></span> 构造子的
    <span class="inlinecode"><span class="id" type="var">nat</span></span> 参数换成了任意的类型 <span class="inlinecode"><span class="id" type="var">X</span></span>，定义的头部添加了 <span class="inlinecode"><span class="id" type="var">X</span></span> 的绑定，
    而构造子类型中的 <span class="inlinecode"><span class="id" type="var">natlist</span></span> 则换成了 <span class="inlinecode"><span class="id" type="var">list</span></span> <span class="inlinecode"><span class="id" type="var">X</span></span>。（我们可以重用构造子名
    <span class="inlinecode"><span class="id" type="var">nil</span></span> 和 <span class="inlinecode"><span class="id" type="var">cons</span></span>，因为之前定义的 <span class="inlinecode"><span class="id" type="var">natlist</span></span> 在当前作用之外的一个 <span class="inlinecode"><span class="id" type="keyword">Module</span></span> 中。）

<div class="paragraph"> </div>

    <span class="inlinecode"><span class="id" type="var">list</span></span> 本身又是什么类型？一种不错的思路就是把 <span class="inlinecode"><span class="id" type="var">list</span></span> 当做从 <span class="inlinecode"><span class="id" type="keyword">Type</span></span>
    类型到 <span class="inlinecode"><span class="id" type="keyword">Inductive</span></span> 归纳定义的<b>函数</b>；或者换种思路，即 <span class="inlinecode"><span class="id" type="var">list</span></span>
    是个从 <span class="inlinecode"><span class="id" type="keyword">Type</span></span> 类型到 <span class="inlinecode"><span class="id" type="keyword">Type</span></span> 类型的函数。对于任何特定的类型 <span class="inlinecode"><span class="id" type="var">X</span></span>，
    类型 <span class="inlinecode"><span class="id" type="var">list</span></span> <span class="inlinecode"><span class="id" type="var">X</span></span> 是一个 <span class="inlinecode"><span class="id" type="keyword">Inductive</span></span> 归纳定义的，元素类型为 <span class="inlinecode"><span class="id" type="var">X</span></span> 的列表的集合。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Check</span> <span class="id" type="var">list</span>.<br/>
<span class="comment">(*&nbsp;===&gt;&nbsp;list&nbsp;:&nbsp;Type&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;Type&nbsp;*)</span><br/>
</div>

<div class="doc">
The parameter <span class="inlinecode"><span class="id" type="var">X</span></span> in the definition of <span class="inlinecode"><span class="id" type="var">list</span></span> automatically
    becomes a parameter to the constructors <span class="inlinecode"><span class="id" type="var">nil</span></span> and <span class="inlinecode"><span class="id" type="var">cons</span></span> &mdash; that
    is, <span class="inlinecode"><span class="id" type="var">nil</span></span> and <span class="inlinecode"><span class="id" type="var">cons</span></span> are now polymorphic constructors; when we use
    them, we must now provide a first argument that is the type of the
    list they are building. For example, <span class="inlinecode"><span class="id" type="var">nil</span></span> <span class="inlinecode"><span class="id" type="var">nat</span></span> constructs the
    empty list of type <span class="inlinecode"><span class="id" type="var">nat</span></span>. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Check</span> (<span class="id" type="var">nil</span> <span class="id" type="var">nat</span>).<br/>
<span class="comment">(*&nbsp;===&gt;&nbsp;nil&nbsp;nat&nbsp;:&nbsp;list&nbsp;nat&nbsp;*)</span><br/>
</div>

<div class="doc">
<span class="inlinecode"><span class="id" type="var">cons</span></span> <span class="inlinecode"><span class="id" type="var">nat</span></span> 与此类似，它将类型为 <span class="inlinecode"><span class="id" type="var">nat</span></span> 的元素添加到类型为
    <span class="inlinecode"><span class="id" type="var">list</span></span> <span class="inlinecode"><span class="id" type="var">nat</span></span> 的列表中。以下示例构造了一个只包含自然数 3 的列表： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Check</span> (<span class="id" type="var">cons</span> <span class="id" type="var">nat</span> 3 (<span class="id" type="var">nil</span> <span class="id" type="var">nat</span>)).<br/>
<span class="comment">(*&nbsp;===&gt;&nbsp;cons&nbsp;nat&nbsp;3&nbsp;(nil&nbsp;nat)&nbsp;:&nbsp;list&nbsp;nat&nbsp;*)</span><br/>
</div>

<div class="doc">
<span class="inlinecode"><span class="id" type="var">nil</span></span> 的类型可能是什么？我们可以从定义中看到 <span class="inlinecode"><span class="id" type="var">list</span></span> <span class="inlinecode"><span class="id" type="var">X</span></span> 的类型，
    它忽略了 <span class="inlinecode"><span class="id" type="var">list</span></span> 的形参 <span class="inlinecode"><span class="id" type="var">X</span></span> 的绑定。<span class="inlinecode"><span class="id" type="keyword">Type</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">list</span></span> <span class="inlinecode"><span class="id" type="var">X</span></span> 并没有解释
    <span class="inlinecode"><span class="id" type="var">X</span></span> 的含义，<span class="inlinecode">(<span class="id" type="var">X</span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" type="keyword">Type</span>)</span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">list</span></span> <span class="inlinecode"><span class="id" type="var">X</span></span> 则比较接近。Coq 对这种情况的记法为
    <span class="inlinecode"><span style='font-size:120%;'>&forall;</span></span> <span class="inlinecode"><span class="id" type="var">X</span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" type="keyword">Type</span>,</span> <span class="inlinecode"><span class="id" type="var">list</span></span> <span class="inlinecode"><span class="id" type="var">X</span></span>： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Check</span> <span class="id" type="var">nil</span>.<br/>
<span class="comment">(*&nbsp;===&gt;&nbsp;nil&nbsp;:&nbsp;forall&nbsp;X&nbsp;:&nbsp;Type,&nbsp;list&nbsp;X&nbsp;*)</span><br/>
</div>

<div class="doc">
类似地，定义中 <span class="inlinecode"><span class="id" type="var">cons</span></span> 看起来像 <span class="inlinecode"><span class="id" type="var">X</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">list</span></span> <span class="inlinecode"><span class="id" type="var">X</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">list</span></span> <span class="inlinecode"><span class="id" type="var">X</span></span>
    然而以此约定来解释 <span class="inlinecode"><span class="id" type="var">X</span></span> 的含义则是类型 <span class="inlinecode"><span style='font-size:120%;'>&forall;</span></span> <span class="inlinecode"><span class="id" type="var">X</span>,</span> <span class="inlinecode"><span class="id" type="var">X</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">list</span></span> <span class="inlinecode"><span class="id" type="var">X</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">list</span></span> <span class="inlinecode"><span class="id" type="var">X</span></span>。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Check</span> <span class="id" type="var">cons</span>.<br/>
<span class="comment">(*&nbsp;===&gt;&nbsp;cons&nbsp;:&nbsp;forall&nbsp;X&nbsp;:&nbsp;Type,&nbsp;X&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;list&nbsp;X&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;list&nbsp;X&nbsp;*)</span><br/>
</div>

<div class="doc">
（关于记法的附注：在 <span class="inlinecode">.<span class="id" type="var">v</span></span> 文件中，量词“forall”会写成字母的形式，
    而在生成的 HTML 和一些设置了显示控制的 IDE 中，<span class="inlinecode"><span style='font-size:120%;'>&forall;</span></span>
    通常会渲染成一般的“倒 A”数学符号，虽然你偶尔还是会看到英文拼写的
    “forall”。这只是排版上的效果，它们的含义没有任何区别。） 
<div class="paragraph"> </div>

 如果在每次使用列表构造子时，都要为它提供类型参数，那样会很麻烦。
    不过我们很快就会看到如何省去这种麻烦。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Check</span> (<span class="id" type="var">cons</span> <span class="id" type="var">nat</span> 2 (<span class="id" type="var">cons</span> <span class="id" type="var">nat</span> 1 (<span class="id" type="var">nil</span> <span class="id" type="var">nat</span>))).<br/>
</div>

<div class="doc">
（这里显式地写出了 <span class="inlinecode"><span class="id" type="var">nil</span></span> 和 <span class="inlinecode"><span class="id" type="var">cons</span></span>，因为我们还没为新版本的列表定义
    <span class="inlinecode"></span> <span class="inlinecode">[]</span> <span class="inlinecode"></span> 和 <span class="inlinecode">::</span> 记法。我们待会儿再干。) 
<div class="paragraph"> </div>

 现在我们可以回过头来定义之前写下的列表处理函数的多态版本了。
    例如 <span class="inlinecode"><span class="id" type="tactic">repeat</span></span>：
</div>
<div class="code code-tight">

<span class="id" type="keyword">Fixpoint</span> <span class="id" type="tactic">repeat</span> (<span class="id" type="var">X</span> : <span class="id" type="keyword">Type</span>) (<span class="id" type="var">x</span> : <span class="id" type="var">X</span>) (<span class="id" type="var">count</span> : <span class="id" type="var">nat</span>) : <span class="id" type="var">list</span> <span class="id" type="var">X</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">count</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;| 0 ⇒ <span class="id" type="var">nil</span> <span class="id" type="var">X</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">S</span> <span class="id" type="var">count'</span> ⇒ <span class="id" type="var">cons</span> <span class="id" type="var">X</span> <span class="id" type="var">x</span> (<span class="id" type="tactic">repeat</span> <span class="id" type="var">X</span> <span class="id" type="var">x</span> <span class="id" type="var">count'</span>)<br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/>
</div>

<div class="doc">
同 <span class="inlinecode"><span class="id" type="var">nil</span></span> 与 <span class="inlinecode"><span class="id" type="var">cons</span></span> 一样，我们可以通过将 <span class="inlinecode"><span class="id" type="tactic">repeat</span></span>
    应用到一个类型、一个该类型的元素以及一个数字来使用它： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Example</span> <span class="id" type="var">test_repeat1</span> :<br/>
&nbsp;&nbsp;<span class="id" type="tactic">repeat</span> <span class="id" type="var">nat</span> 4 2 = <span class="id" type="var">cons</span> <span class="id" type="var">nat</span> 4 (<span class="id" type="var">cons</span> <span class="id" type="var">nat</span> 4 (<span class="id" type="var">nil</span> <span class="id" type="var">nat</span>)).<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
要用 <span class="inlinecode"><span class="id" type="tactic">repeat</span></span> 构造其它种类的列表，
    我们只需通过对应类型的参数将它实例化即可： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Example</span> <span class="id" type="var">test_repeat2</span> :<br/>
&nbsp;&nbsp;<span class="id" type="tactic">repeat</span> <span class="id" type="var">bool</span> <span class="id" type="var">false</span> 1 = <span class="id" type="var">cons</span> <span class="id" type="var">bool</span> <span class="id" type="var">false</span> (<span class="id" type="var">nil</span> <span class="id" type="var">bool</span>).<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a name="lab103"></a><h4 class="section">练习：2 星, standard (mumble_grumble)</h4>
 考虑以下两个归纳定义的类型： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Module</span> <span class="id" type="var">MumbleGrumble</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Inductive</span> <span class="id" type="var">mumble</span> : <span class="id" type="keyword">Type</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">a</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">b</span> (<span class="id" type="var">x</span> : <span class="id" type="var">mumble</span>) (<span class="id" type="var">y</span> : <span class="id" type="var">nat</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">c</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Inductive</span> <span class="id" type="var">grumble</span> (<span class="id" type="var">X</span>:<span class="id" type="keyword">Type</span>) : <span class="id" type="keyword">Type</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">d</span> (<span class="id" type="var">m</span> : <span class="id" type="var">mumble</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">e</span> (<span class="id" type="var">x</span> : <span class="id" type="var">X</span>).<br/>
</div>

<div class="doc">
对于某个类型 <span class="inlinecode"><span class="id" type="var">X</span></span>，以下哪些是 <span class="inlinecode"><span class="id" type="var">grumble</span></span> <span class="inlinecode"><span class="id" type="var">X</span></span> 良定义的元素？
    （在各选项后填“是”或“否”。）

<div class="paragraph"> </div>

<ul class="doclist">
<li> <span class="inlinecode"><span class="id" type="var">d</span></span> <span class="inlinecode">(<span class="id" type="var">b</span></span> <span class="inlinecode"><span class="id" type="var">a</span></span> <span class="inlinecode">5)</span>

</li>
<li> <span class="inlinecode"><span class="id" type="var">d</span></span> <span class="inlinecode"><span class="id" type="var">mumble</span></span> <span class="inlinecode">(<span class="id" type="var">b</span></span> <span class="inlinecode"><span class="id" type="var">a</span></span> <span class="inlinecode">5)</span>

</li>
<li> <span class="inlinecode"><span class="id" type="var">d</span></span> <span class="inlinecode"><span class="id" type="var">bool</span></span> <span class="inlinecode">(<span class="id" type="var">b</span></span> <span class="inlinecode"><span class="id" type="var">a</span></span> <span class="inlinecode">5)</span>

</li>
<li> <span class="inlinecode"><span class="id" type="var">e</span></span> <span class="inlinecode"><span class="id" type="var">bool</span></span> <span class="inlinecode"><span class="id" type="var">true</span></span>

</li>
<li> <span class="inlinecode"><span class="id" type="var">e</span></span> <span class="inlinecode"><span class="id" type="var">mumble</span></span> <span class="inlinecode">(<span class="id" type="var">b</span></span> <span class="inlinecode"><span class="id" type="var">c</span></span> <span class="inlinecode">0)</span>

</li>
<li> <span class="inlinecode"><span class="id" type="var">e</span></span> <span class="inlinecode"><span class="id" type="var">bool</span></span> <span class="inlinecode">(<span class="id" type="var">b</span></span> <span class="inlinecode"><span class="id" type="var">c</span></span> <span class="inlinecode">0)</span>

</li>
<li> <span class="inlinecode"><span class="id" type="var">c</span></span> 
</li>
</ul>

</div>
<div class="code code-tight">
<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/>
<span class="id" type="keyword">End</span> <span class="id" type="var">MumbleGrumble</span>.<br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;请勿修改下面这一行：&nbsp;*)</span><br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">manual_grade_for_mumble_grumble</span> : <span class="id" type="var">option</span> (<span class="id" type="var">nat</span>*<span class="id" type="var">string</span>) := <span class="id" type="var">None</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 

<div class="doc">
<a name="lab104"></a><h3 class="section">类型标注的推断</h3>

<div class="paragraph"> </div>

 我们再写一遍 <span class="inlinecode"><span class="id" type="tactic">repeat</span></span> 的定义，不过这次不指定任何参数的类型。
    Coq 还会接受它么？ 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">repeat'</span> <span class="id" type="var">X</span> <span class="id" type="var">x</span> <span class="id" type="var">count</span> : <span class="id" type="var">list</span> <span class="id" type="var">X</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">count</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;| 0        ⇒ <span class="id" type="var">nil</span> <span class="id" type="var">X</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">S</span> <span class="id" type="var">count'</span> ⇒ <span class="id" type="var">cons</span> <span class="id" type="var">X</span> <span class="id" type="var">x</span> (<span class="id" type="var">repeat'</span> <span class="id" type="var">X</span> <span class="id" type="var">x</span> <span class="id" type="var">count'</span>)<br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/>
</div>

<div class="doc">
当然会。我们来看看 Coq 赋予了 <span class="inlinecode"><span class="id" type="var">repeat'</span></span> 什么类型： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Check</span> <span class="id" type="var">repeat'</span>.<br/>
<span class="comment">(*&nbsp;===&gt;&nbsp;forall&nbsp;X&nbsp;:&nbsp;Type,&nbsp;X&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;nat&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;list&nbsp;X&nbsp;*)</span><br/>
<span class="id" type="keyword">Check</span> <span class="id" type="tactic">repeat</span>.<br/>
<span class="comment">(*&nbsp;===&gt;&nbsp;forall&nbsp;X&nbsp;:&nbsp;Type,&nbsp;X&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;nat&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;list&nbsp;X&nbsp;*)</span><br/>
</div>

<div class="doc">
它与 <span class="inlinecode"><span class="id" type="tactic">repeat</span></span> 的类型完全一致。Coq 可以使用<b>类型推断</b>
    基于它们的使用方式来推出 <span class="inlinecode"><span class="id" type="var">X</span></span>、<span class="inlinecode"><span class="id" type="var">x</span></span> 和 <span class="inlinecode"><span class="id" type="var">count</span></span> 一定是什么类型。例如，
    由于 <span class="inlinecode"><span class="id" type="var">X</span></span> 是作为 <span class="inlinecode"><span class="id" type="var">cons</span></span> 的参数使用的，因此它必定是个 <span class="inlinecode"><span class="id" type="keyword">Type</span></span> 类型，
    因为 <span class="inlinecode"><span class="id" type="var">cons</span></span> 期望一个 <span class="inlinecode"><span class="id" type="keyword">Type</span></span> 作为其第一个参数，而用 <span class="inlinecode">0</span> 和 <span class="inlinecode"><span class="id" type="var">S</span></span> 来匹配
    <span class="inlinecode"><span class="id" type="var">count</span></span> 意味着它必须是个 <span class="inlinecode"><span class="id" type="var">nat</span></span>，诸如此类。

<div class="paragraph"> </div>

    这种强大的功能意味着我们不必总是在任何地方都显式地写出类型标注，
    不过显式的类型标注对于文档和完整性检查来说仍然非常有用，
    因此我们仍会继续使用它。你应当在代码中把握好使用类型标注的平衡点，
    太多导致混乱并分散注意力，太少则会迫使读者为理解你的代码而在大脑中进行类型推断。 
</div>

<div class="doc">
<a name="lab105"></a><h3 class="section">类型参数的推断</h3>

<div class="paragraph"> </div>

 要使用多态函数，我们需要为其参数再额外传入一个或更多类型。
    例如，前面 <span class="inlinecode"><span class="id" type="tactic">repeat</span></span> 函数体中的递归调用必须传递类型 <span class="inlinecode"><span class="id" type="var">X</span></span>。不过由于
    <span class="inlinecode"><span class="id" type="tactic">repeat</span></span> 的第二个参数为 <span class="inlinecode"><span class="id" type="var">X</span></span> 类型的元素，第一个参数明显只能是 <span class="inlinecode"><span class="id" type="var">X</span></span>，
    既然如此，我们何必显式地写出它呢？

<div class="paragraph"> </div>

    Fortunately, Coq permits us to avoid this kind of redundancy.  In
    place of any type argument we can write a "hole" <span class="inlinecode"><span class="id" type="var">_</span></span>, which can be
    read as "Please try to figure out for yourself what belongs here."
    More precisely, when Coq encounters a <span class="inlinecode"><span class="id" type="var">_</span></span>, it will attempt to
    _unify_ all locally available information &mdash; the type of the
    function being applied, the types of the other arguments, and the
    type expected by the context in which the application appears &mdash;
    to determine what concrete type should replace the <span class="inlinecode"><span class="id" type="var">_</span></span>.

<div class="paragraph"> </div>

    这听起来很像类型标注推断。实际上，这两种个过程依赖于同样的底层机制。
    除了简单地忽略函数中某些参数的类型：

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">repeat'</span>&nbsp;<span class="id" type="var">X</span>&nbsp;<span class="id" type="var">x</span>&nbsp;<span class="id" type="var">count</span>&nbsp;:&nbsp;<span class="id" type="var">list</span>&nbsp;<span class="id" type="var">X</span>&nbsp;:=
<div class="paragraph"> </div>

</div>
    我们还可以将类型换成 <span class="inlinecode"><span class="id" type="var">_</span></span>：

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">repeat'</span>&nbsp;(<span class="id" type="var">X</span>&nbsp;:&nbsp;<span class="id" type="var">_</span>)&nbsp;(<span class="id" type="var">x</span>&nbsp;:&nbsp;<span class="id" type="var">_</span>)&nbsp;(<span class="id" type="var">count</span>&nbsp;:&nbsp;<span class="id" type="var">_</span>)&nbsp;:&nbsp;<span class="id" type="var">list</span>&nbsp;<span class="id" type="var">X</span>&nbsp;:=
<div class="paragraph"> </div>

</div>
    以此来告诉 Coq 要尝试推断出缺少的信息。

<div class="paragraph"> </div>

    Using holes, the <span class="inlinecode"><span class="id" type="tactic">repeat</span></span> function can be written like this: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">repeat''</span> <span class="id" type="var">X</span> <span class="id" type="var">x</span> <span class="id" type="var">count</span> : <span class="id" type="var">list</span> <span class="id" type="var">X</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">count</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;| 0        ⇒ <span class="id" type="var">nil</span> <span class="id" type="var">_</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">S</span> <span class="id" type="var">count'</span> ⇒ <span class="id" type="var">cons</span> <span class="id" type="var">_</span> <span class="id" type="var">x</span> (<span class="id" type="var">repeat''</span> <span class="id" type="var">_</span> <span class="id" type="var">x</span> <span class="id" type="var">count'</span>)<br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/>
</div>

<div class="doc">
在此例中，我们写出 <span class="inlinecode"><span class="id" type="var">_</span></span> 并没有省略多少 <span class="inlinecode"><span class="id" type="var">X</span></span>。然而在很多情况下，
    这对减少击键次数和提高可读性还是很有效的。例如，假设我们要写下一个包含数字
    <span class="inlinecode">1</span>、<span class="inlinecode">2</span> 和 <span class="inlinecode">3</span> 的列表，此时不必写成这样： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">list123</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="var">cons</span> <span class="id" type="var">nat</span> 1 (<span class="id" type="var">cons</span> <span class="id" type="var">nat</span> 2 (<span class="id" type="var">cons</span> <span class="id" type="var">nat</span> 3 (<span class="id" type="var">nil</span> <span class="id" type="var">nat</span>))).<br/>
</div>

<div class="doc">
...we can use holes to write this: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">list123'</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="var">cons</span> <span class="id" type="var">_</span> 1 (<span class="id" type="var">cons</span> <span class="id" type="var">_</span> 2 (<span class="id" type="var">cons</span> <span class="id" type="var">_</span> 3 (<span class="id" type="var">nil</span> <span class="id" type="var">_</span>))).<br/>
</div>

<div class="doc">
<a name="lab106"></a><h3 class="section">隐式参数</h3>

<div class="paragraph"> </div>

 我们甚至可以通过告诉 Coq <b>总是</b>推断给定函数的类型参数来避免 <span class="inlinecode"><span class="id" type="var">_</span></span>。

<div class="paragraph"> </div>

    <span class="inlinecode"><span class="id" type="var">Arguments</span></span> 用于指令指定函数或构造子的名字并列出其参数名，
    花括号中的任何参数都会被视作隐式参数。（如果定义中的某个参数没有名字，
    那么它可以用通配模式 <span class="inlinecode"><span class="id" type="var">_</span></span> 来标记。这种情况常见于构造子中。） 
</div>
<div class="code code-tight">

<span class="id" type="var">Arguments</span> <span class="id" type="var">nil</span> {<span class="id" type="var">X</span>}.<br/>
<span class="id" type="var">Arguments</span> <span class="id" type="var">cons</span> {<span class="id" type="var">X</span>} <span class="id" type="var">_</span> <span class="id" type="var">_</span>.<br/>
<span class="id" type="var">Arguments</span> <span class="id" type="tactic">repeat</span> {<span class="id" type="var">X</span>} <span class="id" type="var">x</span> <span class="id" type="var">count</span>.<br/>
</div>

<div class="doc">
现在我们再也不必提供类型参数了： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">list123''</span> := <span class="id" type="var">cons</span> 1 (<span class="id" type="var">cons</span> 2 (<span class="id" type="var">cons</span> 3 <span class="id" type="var">nil</span>)).<br/>
</div>

<div class="doc">
此外，我们还可以在定义函数时声明隐式参数，
    只是需要将它放在花括号内而非圆括号中。例如： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">repeat'''</span> {<span class="id" type="var">X</span> : <span class="id" type="keyword">Type</span>} (<span class="id" type="var">x</span> : <span class="id" type="var">X</span>) (<span class="id" type="var">count</span> : <span class="id" type="var">nat</span>) : <span class="id" type="var">list</span> <span class="id" type="var">X</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">count</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;| 0        ⇒ <span class="id" type="var">nil</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">S</span> <span class="id" type="var">count'</span> ⇒ <span class="id" type="var">cons</span> <span class="id" type="var">x</span> (<span class="id" type="var">repeat'''</span> <span class="id" type="var">x</span> <span class="id" type="var">count'</span>)<br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/>
</div>

<div class="doc">
（注意我们现在甚至不必在 <span class="inlinecode"><span class="id" type="var">repeat'''</span></span> 的递归调用中提供类型参数了，
      实际上提供了反而是无效的！）

<div class="paragraph"> </div>

    我们会尽可能使用最后一种风格，不过还会继续在 <span class="inlinecode"><span class="id" type="keyword">Inductive</span></span> 构造子中使用显式的
    <span class="inlinecode"><span class="id" type="var">Argument</span></span> 声明。原因在于如果将归纳类型的形参标为隐式的话，
    不仅构造子的类型会变成隐式的，类型本身也会变成隐式的。例如，
    考虑以下 <span class="inlinecode"><span class="id" type="var">list</span></span> 类型的另一种定义： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">list'</span> {<span class="id" type="var">X</span>:<span class="id" type="keyword">Type</span>} : <span class="id" type="keyword">Type</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">nil'</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">cons'</span> (<span class="id" type="var">x</span> : <span class="id" type="var">X</span>) (<span class="id" type="var">l</span> : <span class="id" type="var">list'</span>).<br/>
</div>

<div class="doc">
由于 <span class="inlinecode"><span class="id" type="var">X</span></span> 在包括 <span class="inlinecode"><span class="id" type="var">list'</span></span> 本身的<b>整个</b>归纳定义中都是隐式声明的，
    因此当我们讨论数值、布尔值或其它任何类型的列表时，都只能写 <span class="inlinecode"><span class="id" type="var">list'</span></span>，
    而写不了 <span class="inlinecode"><span class="id" type="var">list'</span></span> <span class="inlinecode"><span class="id" type="var">nat</span></span>、<span class="inlinecode"><span class="id" type="var">list'</span></span> <span class="inlinecode"><span class="id" type="var">bool</span></span> 或其它的了，这样就跑得有点太远了。 
<div class="paragraph"> </div>

 作为本节的收尾，我们为新的多态列表重新实现几个其它的标准列表函数... 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">app</span> {<span class="id" type="var">X</span> : <span class="id" type="keyword">Type</span>} (<span class="id" type="var">l<sub>1</sub></span> <span class="id" type="var">l<sub>2</sub></span> : <span class="id" type="var">list</span> <span class="id" type="var">X</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;: (<span class="id" type="var">list</span> <span class="id" type="var">X</span>) :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">l<sub>1</sub></span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">nil</span>      ⇒ <span class="id" type="var">l<sub>2</sub></span><br/>
&nbsp;&nbsp;| <span class="id" type="var">cons</span> <span class="id" type="var">h</span> <span class="id" type="var">t</span> ⇒ <span class="id" type="var">cons</span> <span class="id" type="var">h</span> (<span class="id" type="var">app</span> <span class="id" type="var">t</span> <span class="id" type="var">l<sub>2</sub></span>)<br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">rev</span> {<span class="id" type="var">X</span>:<span class="id" type="keyword">Type</span>} (<span class="id" type="var">l</span>:<span class="id" type="var">list</span> <span class="id" type="var">X</span>) : <span class="id" type="var">list</span> <span class="id" type="var">X</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">l</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">nil</span>      ⇒ <span class="id" type="var">nil</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">cons</span> <span class="id" type="var">h</span> <span class="id" type="var">t</span> ⇒ <span class="id" type="var">app</span> (<span class="id" type="var">rev</span> <span class="id" type="var">t</span>) (<span class="id" type="var">cons</span> <span class="id" type="var">h</span> <span class="id" type="var">nil</span>)<br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">length</span> {<span class="id" type="var">X</span> : <span class="id" type="keyword">Type</span>} (<span class="id" type="var">l</span> : <span class="id" type="var">list</span> <span class="id" type="var">X</span>) : <span class="id" type="var">nat</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">l</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">nil</span> ⇒ 0<br/>
&nbsp;&nbsp;| <span class="id" type="var">cons</span> <span class="id" type="var">_</span> <span class="id" type="var">l'</span> ⇒ <span class="id" type="var">S</span> (<span class="id" type="var">length</span> <span class="id" type="var">l'</span>)<br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_rev1</span> :<br/>
&nbsp;&nbsp;<span class="id" type="var">rev</span> (<span class="id" type="var">cons</span> 1 (<span class="id" type="var">cons</span> 2 <span class="id" type="var">nil</span>)) = (<span class="id" type="var">cons</span> 2 (<span class="id" type="var">cons</span> 1 <span class="id" type="var">nil</span>)).<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_rev2</span>:<br/>
&nbsp;&nbsp;<span class="id" type="var">rev</span> (<span class="id" type="var">cons</span> <span class="id" type="var">true</span> <span class="id" type="var">nil</span>) = <span class="id" type="var">cons</span> <span class="id" type="var">true</span> <span class="id" type="var">nil</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_length1</span>: <span class="id" type="var">length</span> (<span class="id" type="var">cons</span> 1 (<span class="id" type="var">cons</span> 2 (<span class="id" type="var">cons</span> 3 <span class="id" type="var">nil</span>))) = 3.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a name="lab107"></a><h3 class="section">显式提供类型参数</h3>

<div class="paragraph"> </div>

 用 <span class="inlinecode"><span class="id" type="keyword">Implicit</span></span> 将参数声明为隐式的会有个小问题：Coq
    偶尔会没有足够的局部信息来确定类型参数。此时，我们需要告诉 Coq
    这次我们会显示地给出参数。例如，假设我们写了如下定义： 
</div>
<div class="code code-tight">

<span class="id" type="var">Fail</span> <span class="id" type="keyword">Definition</span> <span class="id" type="var">mynil</span> := <span class="id" type="var">nil</span>.<br/>
</div>

<div class="doc">
（<span class="inlinecode"><span class="id" type="keyword">Definition</span></span> 前面的 <span class="inlinecode"><span class="id" type="var">Fail</span></span> 限定符可用于<b>任何</b>指令，
    它的作用是确保该指令在执行时确实会失败。如果该指令失败了，Coq
    就会打印出相应的错误信息，不过之后会继续处理文件中剩下的部分。）

<div class="paragraph"> </div>

    在这里，Coq 给出了一条错误信息，因为它不知道应该为 <span class="inlinecode"><span class="id" type="var">nil</span></span> 提供何种类型。
    我们可以为它提供个显式的类型声明来帮助它，这样 Coq 在“应用”<span class="inlinecode"><span class="id" type="var">nil</span></span>
    时就有更多可用的信息了： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">mynil</span> : <span class="id" type="var">list</span> <span class="id" type="var">nat</span> := <span class="id" type="var">nil</span>.<br/>
</div>

<div class="doc">
此外，我们还可以在函数名前加上前缀 <span class="inlinecode">@</span> 来强制将隐式参数变成显式的： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Check</span> @<span class="id" type="var">nil</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">mynil'</span> := @<span class="id" type="var">nil</span> <span class="id" type="var">nat</span>.<br/>
</div>

<div class="doc">
使用参数推断和隐式参数，我们可以为列表定义和前面一样的简便记法。
    由于我们让构造子的的类型参数变成了隐式的，因此 Coq
    就知道在我们使用该记法时自动推断它们了。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Notation</span> "x :: y" := (<span class="id" type="var">cons</span> <span class="id" type="var">x</span> <span class="id" type="var">y</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="tactic">at</span> <span class="id" type="var">level</span> 60, <span class="id" type="var">right</span> <span class="id" type="var">associativity</span>).<br/>
<span class="id" type="keyword">Notation</span> "[ ]" := <span class="id" type="var">nil</span>.<br/>
<span class="id" type="keyword">Notation</span> "[ x ; .. ; y ]" := (<span class="id" type="var">cons</span> <span class="id" type="var">x</span> .. (<span class="id" type="var">cons</span> <span class="id" type="var">y</span> []) ..).<br/>
<span class="id" type="keyword">Notation</span> "x ++ y" := (<span class="id" type="var">app</span> <span class="id" type="var">x</span> <span class="id" type="var">y</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="tactic">at</span> <span class="id" type="var">level</span> 60, <span class="id" type="var">right</span> <span class="id" type="var">associativity</span>).<br/>
</div>

<div class="doc">
现在列表就能写成我们希望的方式了： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">list123'''</span> := [1; 2; 3].<br/>
</div>

<div class="doc">
<a name="lab108"></a><h3 class="section">练习</h3>

<div class="paragraph"> </div>

<a name="lab109"></a><h4 class="section">练习：2 星, standard, optional (poly_exercises)</h4>
 下面是一些简单的练习，和 <span class="inlinecode"><span class="id" type="var">Lists</span></span> 一章中的一样。
    为了实践多态，请完成下面的证明。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">app_nil_r</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">X</span>:<span class="id" type="keyword">Type</span>), <span style='font-size:120%;'>&forall;</span><span class="id" type="var">l</span>:<span class="id" type="var">list</span> <span class="id" type="var">X</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">l</span> ++ [] = <span class="id" type="var">l</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">app_assoc</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">A</span> (<span class="id" type="var">l</span> <span class="id" type="var">m</span> <span class="id" type="var">n</span>:<span class="id" type="var">list</span> <span class="id" type="var">A</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">l</span> ++ <span class="id" type="var">m</span> ++ <span class="id" type="var">n</span> = (<span class="id" type="var">l</span> ++ <span class="id" type="var">m</span>) ++ <span class="id" type="var">n</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">app_length</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">X</span>:<span class="id" type="keyword">Type</span>) (<span class="id" type="var">l<sub>1</sub></span> <span class="id" type="var">l<sub>2</sub></span> : <span class="id" type="var">list</span> <span class="id" type="var">X</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">length</span> (<span class="id" type="var">l<sub>1</sub></span> ++ <span class="id" type="var">l<sub>2</sub></span>) = <span class="id" type="var">length</span> <span class="id" type="var">l<sub>1</sub></span> + <span class="id" type="var">length</span> <span class="id" type="var">l<sub>2</sub></span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab110"></a><h4 class="section">练习：2 星, standard, optional (more_poly_exercises)</h4>
 这儿有些更有趣的东西... 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">rev_app_distr</span>: <span style='font-size:120%;'>&forall;</span><span class="id" type="var">X</span> (<span class="id" type="var">l<sub>1</sub></span> <span class="id" type="var">l<sub>2</sub></span> : <span class="id" type="var">list</span> <span class="id" type="var">X</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">rev</span> (<span class="id" type="var">l<sub>1</sub></span> ++ <span class="id" type="var">l<sub>2</sub></span>) = <span class="id" type="var">rev</span> <span class="id" type="var">l<sub>2</sub></span> ++ <span class="id" type="var">rev</span> <span class="id" type="var">l<sub>1</sub></span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">rev_involutive</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">X</span> : <span class="id" type="keyword">Type</span>, <span style='font-size:120%;'>&forall;</span><span class="id" type="var">l</span> : <span class="id" type="var">list</span> <span class="id" type="var">X</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">rev</span> (<span class="id" type="var">rev</span> <span class="id" type="var">l</span>) = <span class="id" type="var">l</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 

<div class="doc">
<a name="lab111"></a><h2 class="section">多态序对</h2>

<div class="paragraph"> </div>

 按照相同的模式，我们在上一章中给出的数值序对的定义可被推广为
    <b>多态序对（Polymorphic Pairs）</b>，它通常叫做<b>积（Products）</b>： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">prod</span> (<span class="id" type="var">X</span> <span class="id" type="var">Y</span> : <span class="id" type="keyword">Type</span>) : <span class="id" type="keyword">Type</span> :=<br/>
| <span class="id" type="var">pair</span> (<span class="id" type="var">x</span> : <span class="id" type="var">X</span>) (<span class="id" type="var">y</span> : <span class="id" type="var">Y</span>).<br/><hr class='doublespaceincode'/>
<span class="id" type="var">Arguments</span> <span class="id" type="var">pair</span> {<span class="id" type="var">X</span>} {<span class="id" type="var">Y</span>} <span class="id" type="var">_</span> <span class="id" type="var">_</span>.<br/>
</div>

<div class="doc">
和列表一样，我们也可以将类型参数定义成隐式的，
    并以此定义类似的具体记法： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Notation</span> "( x , y )" := (<span class="id" type="var">pair</span> <span class="id" type="var">x</span> <span class="id" type="var">y</span>).<br/>
</div>

<div class="doc">
我们也可以使用 <span class="inlinecode"><span class="id" type="keyword">Notation</span></span> 来定义标准的<b>积类型（Product Types）</b>记法： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Notation</span> "X * Y" := (<span class="id" type="var">prod</span> <span class="id" type="var">X</span> <span class="id" type="var">Y</span>) : <span class="id" type="var">type_scope</span>.<br/>
</div>

<div class="doc">
（标注 <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" type="var">type_scope</span></span> 会告诉 Coq 该缩写只能在解析类型时使用。
      这避免了与乘法符号的冲突。) 
<div class="paragraph"> </div>

 一开始会很容易混淆 <span class="inlinecode">(<span class="id" type="var">x</span>,<span class="id" type="var">y</span>)</span> 和 <span class="inlinecode"><span class="id" type="var">X</span>*<span class="id" type="var">Y</span></span>。不过要记住 <span class="inlinecode">(<span class="id" type="var">x</span>,<span class="id" type="var">y</span>)</span>
    是一个<b>值</b>，它由两个其它的值构造得来；而 <span class="inlinecode"><span class="id" type="var">X</span>*<span class="id" type="var">Y</span></span> 是一个<b>类型</b>，
    它由两个其它的类型构造得来。如果 <span class="inlinecode"><span class="id" type="var">x</span></span> 的类型为 <span class="inlinecode"><span class="id" type="var">X</span></span> 而 <span class="inlinecode"><span class="id" type="var">y</span></span> 的类型为 <span class="inlinecode"><span class="id" type="var">Y</span></span>，
    那么 <span class="inlinecode">(<span class="id" type="var">x</span>,<span class="id" type="var">y</span>)</span> 的类型就是 <span class="inlinecode"><span class="id" type="var">X</span>*<span class="id" type="var">Y</span></span>。 
<div class="paragraph"> </div>

 第一元（first）和第二元（second）的射影函数（Projection Functions）
    现在看起来和其它函数式编程语言中的很像了： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">fst</span> {<span class="id" type="var">X</span> <span class="id" type="var">Y</span> : <span class="id" type="keyword">Type</span>} (<span class="id" type="var">p</span> : <span class="id" type="var">X</span> * <span class="id" type="var">Y</span>) : <span class="id" type="var">X</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">p</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;| (<span class="id" type="var">x</span>, <span class="id" type="var">y</span>) ⇒ <span class="id" type="var">x</span><br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">snd</span> {<span class="id" type="var">X</span> <span class="id" type="var">Y</span> : <span class="id" type="keyword">Type</span>} (<span class="id" type="var">p</span> : <span class="id" type="var">X</span> * <span class="id" type="var">Y</span>) : <span class="id" type="var">Y</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">p</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;| (<span class="id" type="var">x</span>, <span class="id" type="var">y</span>) ⇒ <span class="id" type="var">y</span><br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/>
</div>

<div class="doc">
以下函数接受两个列表，并将它们结合成一个序对的列表。
    在其它函数式语言中，它通常被称作 <span class="inlinecode"><span class="id" type="var">zip</span></span>。我们为了与 Coq 的标准库保持一致，
    将它命名为 <span class="inlinecode"><span class="id" type="var">combine</span></span>。
</div>
<div class="code code-tight">

<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">combine</span> {<span class="id" type="var">X</span> <span class="id" type="var">Y</span> : <span class="id" type="keyword">Type</span>} (<span class="id" type="var">lx</span> : <span class="id" type="var">list</span> <span class="id" type="var">X</span>) (<span class="id" type="var">ly</span> : <span class="id" type="var">list</span> <span class="id" type="var">Y</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;: <span class="id" type="var">list</span> (<span class="id" type="var">X</span>*<span class="id" type="var">Y</span>) :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">lx</span>, <span class="id" type="var">ly</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;| [], <span class="id" type="var">_</span> ⇒ []<br/>
&nbsp;&nbsp;| <span class="id" type="var">_</span>, [] ⇒ []<br/>
&nbsp;&nbsp;| <span class="id" type="var">x</span> :: <span class="id" type="var">tx</span>, <span class="id" type="var">y</span> :: <span class="id" type="var">ty</span> ⇒ (<span class="id" type="var">x</span>, <span class="id" type="var">y</span>) :: (<span class="id" type="var">combine</span> <span class="id" type="var">tx</span> <span class="id" type="var">ty</span>)<br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/>
</div>

<div class="doc">
<a name="lab112"></a><h4 class="section">练习：1 星, standard, optional (combine_checks)</h4>
 请尝试在纸上回答以下问题并在 Coq 中检验你的解答：

<div class="paragraph"> </div>

<ul class="doclist">
<li> <span class="inlinecode"><span class="id" type="var">combine</span></span> 的类型是什么？（即 <span class="inlinecode"><span class="id" type="keyword">Check</span></span> <span class="inlinecode">@<span class="id" type="var">combine</span></span> 会打印出什么？）

</li>
<li> 以下指令会打印出什么？

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;<span class="id" type="var">Compute</span>&nbsp;(<span class="id" type="var">combine</span>&nbsp;[1;2]&nbsp;[<span class="id" type="var">false</span>;<span class="id" type="var">false</span>;<span class="id" type="var">true</span>;<span class="id" type="var">true</span>]).
<div class="paragraph"> </div>

</div>

</li>
</ul>
 <span class="proofbox">&#9744;</span> 
<div class="paragraph"> </div>

<a name="lab113"></a><h4 class="section">练习：2 星, standard, recommended (split)</h4>
 函数 <span class="inlinecode"><span class="id" type="tactic">split</span></span> 是 <span class="inlinecode"><span class="id" type="var">combine</span></span> 的右逆（right inverse）：
    它接受一个序对的列表并返回一个列表的序对。
    在很多函数式语言中，它被称作 <span class="inlinecode"><span class="id" type="var">unzip</span></span>。

<div class="paragraph"> </div>

    请在下面完成 <span class="inlinecode"><span class="id" type="tactic">split</span></span> 的定义，确保它能够通过给定的单元测试。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Fixpoint</span> <span class="id" type="tactic">split</span> {<span class="id" type="var">X</span> <span class="id" type="var">Y</span> : <span class="id" type="keyword">Type</span>} (<span class="id" type="var">l</span> : <span class="id" type="var">list</span> (<span class="id" type="var">X</span>*<span class="id" type="var">Y</span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;: (<span class="id" type="var">list</span> <span class="id" type="var">X</span>) * (<span class="id" type="var">list</span> <span class="id" type="var">Y</span>)<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;将本行替换成&nbsp;":=&nbsp;_你的_定义_&nbsp;."&nbsp;*)</span>. <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_split</span>:<br/>
&nbsp;&nbsp;<span class="id" type="tactic">split</span> [(1,<span class="id" type="var">false</span>);(2,<span class="id" type="var">false</span>)] = ([1;2],[<span class="id" type="var">false</span>;<span class="id" type="var">false</span>]).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 

<div class="doc">
<a name="lab114"></a><h2 class="section">多态候选</h2>

<div class="paragraph"> </div>

 现在介绍最后一种多态类型：<b>多态候选（Polymorphic Options）</b>,
    它推广了上一章中的 <span class="inlinecode"><span class="id" type="var">natoption</span></span>：  One last polymorphic type for now: _polymorphic options_,
    which generalize <span class="inlinecode"><span class="id" type="var">natoption</span></span> from the previous chapter.  (We put
    the definition inside a module because the standard library
    already defines <span class="inlinecode"><span class="id" type="var">option</span></span> and it's this one that we want to use
    below.) 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Module</span> <span class="id" type="var">OptionPlayground</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Inductive</span> <span class="id" type="var">option</span> (<span class="id" type="var">X</span>:<span class="id" type="keyword">Type</span>) : <span class="id" type="keyword">Type</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">Some</span> (<span class="id" type="var">x</span> : <span class="id" type="var">X</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">None</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="var">Arguments</span> <span class="id" type="var">Some</span> {<span class="id" type="var">X</span>} <span class="id" type="var">_</span>.<br/>
<span class="id" type="var">Arguments</span> <span class="id" type="var">None</span> {<span class="id" type="var">X</span>}.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">End</span> <span class="id" type="var">OptionPlayground</span>.<br/>
</div>

<div class="doc">
现在我们可以重写 <span class="inlinecode"><span class="id" type="var">nth_error</span></span> 函数来让它适用于任何类型的列表了。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">nth_error</span> {<span class="id" type="var">X</span> : <span class="id" type="keyword">Type</span>} (<span class="id" type="var">l</span> : <span class="id" type="var">list</span> <span class="id" type="var">X</span>) (<span class="id" type="var">n</span> : <span class="id" type="var">nat</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;: <span class="id" type="var">option</span> <span class="id" type="var">X</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">l</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;| [] ⇒ <span class="id" type="var">None</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">a</span> :: <span class="id" type="var">l'</span> ⇒ <span class="id" type="keyword">if</span> <span class="id" type="var">n</span> =? <span class="id" type="var">O</span> <span class="id" type="keyword">then</span> <span class="id" type="var">Some</span> <span class="id" type="var">a</span> <span class="id" type="keyword">else</span> <span class="id" type="var">nth_error</span> <span class="id" type="var">l'</span> (<span class="id" type="var">pred</span> <span class="id" type="var">n</span>)<br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_nth_error1</span> : <span class="id" type="var">nth_error</span> [4;5;6;7] 0 = <span class="id" type="var">Some</span> 4.<br/>
<div class="togglescript" id="proofcontrol1" onclick="toggleDisplay('proof1');toggleDisplay('proofcontrol1')"><span class="show"></span></div>
<div class="proofscript" id="proof1" onclick="toggleDisplay('proof1');toggleDisplay('proofcontrol1')">
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_nth_error2</span> : <span class="id" type="var">nth_error</span> [[1];[2]] 1 = <span class="id" type="var">Some</span> [2].<br/>
<div class="togglescript" id="proofcontrol2" onclick="toggleDisplay('proof2');toggleDisplay('proofcontrol2')"><span class="show"></span></div>
<div class="proofscript" id="proof2" onclick="toggleDisplay('proof2');toggleDisplay('proofcontrol2')">
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_nth_error3</span> : <span class="id" type="var">nth_error</span> [<span class="id" type="var">true</span>] 2 = <span class="id" type="var">None</span>.<br/>
<div class="togglescript" id="proofcontrol3" onclick="toggleDisplay('proof3');toggleDisplay('proofcontrol3')"><span class="show"></span></div>
<div class="proofscript" id="proof3" onclick="toggleDisplay('proof3');toggleDisplay('proofcontrol3')">
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
<a name="lab115"></a><h4 class="section">练习：1 星, standard, optional (hd_error_poly)</h4>
 请完成上一章中 <span class="inlinecode"><span class="id" type="var">hd_error</span></span> 的多态定义，确保它能通过下方的单元测试。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">hd_error</span> {<span class="id" type="var">X</span> : <span class="id" type="keyword">Type</span>} (<span class="id" type="var">l</span> : <span class="id" type="var">list</span> <span class="id" type="var">X</span>) : <span class="id" type="var">option</span> <span class="id" type="var">X</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;将本行替换成&nbsp;":=&nbsp;_你的_定义_&nbsp;."&nbsp;*)</span>. <span class="id" type="var">Admitted</span>.<br/>
</div>

<div class="doc">
再说一遍，要强制将隐式参数转为显式参数，我们可以在函数名前使用 <span class="inlinecode">@</span>。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Check</span> @<span class="id" type="var">hd_error</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_hd_error1</span> : <span class="id" type="var">hd_error</span> [1;2] = <span class="id" type="var">Some</span> 1.<br/>
&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_hd_error2</span> : <span class="id" type="var">hd_error</span>  [[1];[2]]  = <span class="id" type="var">Some</span> [1].<br/>
&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 

<div class="doc">
<a name="lab116"></a><h1 class="section">函数作为数据</h1>

<div class="paragraph"> </div>

 和其它现代编程语言，包括所有函数式语言（ML、Haskell、
    Scheme、Scala、Clojure 等）一样，Coq 也将函数视作“一等公民（First-Class Citizens）”，
    即允许将它们作为参数传入其它函数、作为结果返回、以及存储在数据结构中等等。 
</div>

<div class="doc">
<a name="lab117"></a><h2 class="section">高阶函数</h2>

<div class="paragraph"> </div>

 用于操作其它函数的函数通常叫做<b>高阶函数</b>。以下是简单的示例： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">doit3times</span> {<span class="id" type="var">X</span>:<span class="id" type="keyword">Type</span>} (<span class="id" type="var">f</span>:<span class="id" type="var">X</span>→<span class="id" type="var">X</span>) (<span class="id" type="var">n</span>:<span class="id" type="var">X</span>) : <span class="id" type="var">X</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="var">f</span> (<span class="id" type="var">f</span> (<span class="id" type="var">f</span> <span class="id" type="var">n</span>)).<br/>
</div>

<div class="doc">
这里的参数 <span class="inlinecode"><span class="id" type="var">f</span></span> 本身也是个（从 <span class="inlinecode"><span class="id" type="var">X</span></span> 到 <span class="inlinecode"><span class="id" type="var">X</span></span> 的）函数，
    <span class="inlinecode"><span class="id" type="var">doit3times</span></span> 的函数体将 <span class="inlinecode"><span class="id" type="var">f</span></span> 对某个值 <span class="inlinecode"><span class="id" type="var">n</span></span> 应用三次。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Check</span> @<span class="id" type="var">doit3times</span>.<br/>
<span class="comment">(*&nbsp;===&gt;&nbsp;doit3times&nbsp;:&nbsp;forall&nbsp;X&nbsp;:&nbsp;Type,&nbsp;(X&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;X)&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;X&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;X&nbsp;*)</span><br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_doit3times</span>: <span class="id" type="var">doit3times</span> <span class="id" type="var">minustwo</span> 9 = 3.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_doit3times'</span>: <span class="id" type="var">doit3times</span> <span class="id" type="var">negb</span> <span class="id" type="var">true</span> = <span class="id" type="var">false</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a name="lab118"></a><h2 class="section">过滤器</h2>

<div class="paragraph"> </div>

 下面是个更有用的高阶函数，它接受一个元素类型为 <span class="inlinecode"><span class="id" type="var">X</span></span> 的列表和一个
    <span class="inlinecode"><span class="id" type="var">X</span></span> 的谓词（即一个从 <span class="inlinecode"><span class="id" type="var">X</span></span> 到 <span class="inlinecode"><span class="id" type="var">bool</span></span> 的函数），然后“过滤”此列表并返回一个新列表，
    其中仅包含对该谓词返回 <span class="inlinecode"><span class="id" type="var">true</span></span> 的元素。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">filter</span> {<span class="id" type="var">X</span>:<span class="id" type="keyword">Type</span>} (<span class="id" type="var">test</span>: <span class="id" type="var">X</span>→<span class="id" type="var">bool</span>) (<span class="id" type="var">l</span>:<span class="id" type="var">list</span> <span class="id" type="var">X</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;: (<span class="id" type="var">list</span> <span class="id" type="var">X</span>) :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">l</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;| []     ⇒ []<br/>
&nbsp;&nbsp;| <span class="id" type="var">h</span> :: <span class="id" type="var">t</span> ⇒ <span class="id" type="keyword">if</span> <span class="id" type="var">test</span> <span class="id" type="var">h</span> <span class="id" type="keyword">then</span> <span class="id" type="var">h</span> :: (<span class="id" type="var">filter</span> <span class="id" type="var">test</span> <span class="id" type="var">t</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">else</span>       <span class="id" type="var">filter</span> <span class="id" type="var">test</span> <span class="id" type="var">t</span><br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/>
</div>

<div class="doc">
例如，如果我们将 <span class="inlinecode"><span class="id" type="var">filter</span></span> 应用到谓词 <span class="inlinecode"><span class="id" type="var">evenb</span></span> 和一个数值列表 <span class="inlinecode"><span class="id" type="var">l</span></span>
    上，那么它就会返回一个只包含 <span class="inlinecode"><span class="id" type="var">l</span></span> 中偶数的列表。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Example</span> <span class="id" type="var">test_filter1</span>: <span class="id" type="var">filter</span> <span class="id" type="var">evenb</span> [1;2;3;4] = [2;4].<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">length_is_1</span> {<span class="id" type="var">X</span> : <span class="id" type="keyword">Type</span>} (<span class="id" type="var">l</span> : <span class="id" type="var">list</span> <span class="id" type="var">X</span>) : <span class="id" type="var">bool</span> :=<br/>
&nbsp;&nbsp;(<span class="id" type="var">length</span> <span class="id" type="var">l</span>) =? 1.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_filter2</span>:<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">filter</span> <span class="id" type="var">length_is_1</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;[ [1; 2]; [3]; [4]; [5;6;7]; []; [8] ]<br/>
&nbsp;&nbsp;= [ [3]; [4]; [8] ].<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
我们可以使用 <span class="inlinecode"><span class="id" type="var">filter</span></span> 给出 <a href="Lists.html"><span class="inlineref">Lists</span></a> 中 <span class="inlinecode"><span class="id" type="var">countoddmembers</span></span>
    函数的简洁的版本。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">countoddmembers'</span> (<span class="id" type="var">l</span>:<span class="id" type="var">list</span> <span class="id" type="var">nat</span>) : <span class="id" type="var">nat</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="var">length</span> (<span class="id" type="var">filter</span> <span class="id" type="var">oddb</span> <span class="id" type="var">l</span>).<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_countoddmembers'1</span>:   <span class="id" type="var">countoddmembers'</span> [1;0;3;1;4;5] = 4.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_countoddmembers'2</span>:   <span class="id" type="var">countoddmembers'</span> [0;2;4] = 0.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_countoddmembers'3</span>:   <span class="id" type="var">countoddmembers'</span> <span class="id" type="var">nil</span> = 0.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a name="lab119"></a><h2 class="section">匿名函数</h2>

<div class="paragraph"> </div>

 在上面这个例子中，我们不得不定义一个名为 <span class="inlinecode"><span class="id" type="var">length_is_1</span></span> 的函数，
    以便让它能够作为参数传入到 <span class="inlinecode"><span class="id" type="var">filter</span></span> 中，由于该函数可能再也用不到了，
    这有点令人沮丧。我们经常需要传入“一次性”的函数作为参数，之后不会再用，
    而为每个函数取名是十分无聊的。

<div class="paragraph"> </div>

    幸运的是，有一种更好的方法。我们可以按需随时构造函数而不必在顶层中声明它
    或给它取名。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Example</span> <span class="id" type="var">test_anon_fun'</span>:<br/>
&nbsp;&nbsp;<span class="id" type="var">doit3times</span> (<span class="id" type="keyword">fun</span> <span class="id" type="var">n</span> ⇒ <span class="id" type="var">n</span> * <span class="id" type="var">n</span>) 2 = 256.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
表达式 <span class="inlinecode">(<span class="id" type="keyword">fun</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">⇒</span> <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">*</span> <span class="inlinecode"><span class="id" type="var">n</span>)</span> 可读作“一个给定 <span class="inlinecode"><span class="id" type="var">n</span></span> 并返回 <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">*</span> <span class="inlinecode"><span class="id" type="var">n</span></span> 的函数。” 
<div class="paragraph"> </div>

 以下为使用匿名函数重写的 <span class="inlinecode"><span class="id" type="var">filter</span></span> 示例：
</div>
<div class="code code-tight">

<span class="id" type="keyword">Example</span> <span class="id" type="var">test_filter2'</span>:<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">filter</span> (<span class="id" type="keyword">fun</span> <span class="id" type="var">l</span> ⇒ (<span class="id" type="var">length</span> <span class="id" type="var">l</span>) =? 1)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;[ [1; 2]; [3]; [4]; [5;6;7]; []; [8] ]<br/>
&nbsp;&nbsp;= [ [3]; [4]; [8] ].<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a name="lab120"></a><h4 class="section">练习：2 星, standard (filter_even_gt<sub>7</sub>)</h4>
 使用 <span class="inlinecode"><span class="id" type="var">filter</span></span>（而非 <span class="inlinecode"><span class="id" type="keyword">Fixpoint</span></span>）来编写 Coq 函数 <span class="inlinecode"><span class="id" type="var">filter_even_gt<sub>7</sub></span></span>，
    它接受一个自然数列表作为输入，返回一个只包含大于 <span class="inlinecode">7</span> 的偶数的列表。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">filter_even_gt<sub>7</sub></span> (<span class="id" type="var">l</span> : <span class="id" type="var">list</span> <span class="id" type="var">nat</span>) : <span class="id" type="var">list</span> <span class="id" type="var">nat</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;将本行替换成&nbsp;":=&nbsp;_你的_定义_&nbsp;."&nbsp;*)</span>. <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_filter_even_gt7_1</span> :<br/>
&nbsp;&nbsp;<span class="id" type="var">filter_even_gt<sub>7</sub></span> [1;2;6;9;10;3;12;8] = [10;12;8].<br/>
&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_filter_even_gt7_2</span> :<br/>
&nbsp;&nbsp;<span class="id" type="var">filter_even_gt<sub>7</sub></span> [5;2;6;19;129] = [].<br/>
&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab121"></a><h4 class="section">练习：3 星, standard (partition)</h4>
 使用 <span class="inlinecode"><span class="id" type="var">filter</span></span> 编写一个 Coq 函数 <span class="inlinecode"><span class="id" type="var">partition</span></span>：

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">partition</span>&nbsp;:&nbsp;<span style='font-size:120%;'>&forall;</span><span class="id" type="var">X</span>&nbsp;:&nbsp;<span class="id" type="keyword">Type</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">X</span>&nbsp;→&nbsp;<span class="id" type="var">bool</span>)&nbsp;→&nbsp;<span class="id" type="var">list</span>&nbsp;<span class="id" type="var">X</span>&nbsp;→&nbsp;<span class="id" type="var">list</span>&nbsp;<span class="id" type="var">X</span>&nbsp;*&nbsp;<span class="id" type="var">list</span>&nbsp;<span class="id" type="var">X</span>
<div class="paragraph"> </div>

</div>
   给定一个集合 <span class="inlinecode"><span class="id" type="var">X</span></span>、一个类型为 <span class="inlinecode"><span class="id" type="var">X</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">bool</span></span> 的测试函数和一个 <span class="inlinecode"><span class="id" type="var">list</span></span> <span class="inlinecode"><span class="id" type="var">X</span></span>，
   <span class="inlinecode"><span class="id" type="var">partition</span></span> 应当返回一个列表的序对。该序对的第一个成员为包含原始列表中
   满足该测试的子列表，而第二个成员为包含不满足该测试的元素的子列表。
   两个子列表中元素的顺序应当与它们在原始列表中的顺序相同。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">partition</span> {<span class="id" type="var">X</span> : <span class="id" type="keyword">Type</span>}<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">test</span> : <span class="id" type="var">X</span> → <span class="id" type="var">bool</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">l</span> : <span class="id" type="var">list</span> <span class="id" type="var">X</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;: <span class="id" type="var">list</span> <span class="id" type="var">X</span> * <span class="id" type="var">list</span> <span class="id" type="var">X</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;将本行替换成&nbsp;":=&nbsp;_你的_定义_&nbsp;."&nbsp;*)</span>. <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_partition1</span>: <span class="id" type="var">partition</span> <span class="id" type="var">oddb</span> [1;2;3;4;5] = ([1;3;5], [2;4]).<br/>
<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_partition2</span>: <span class="id" type="var">partition</span> (<span class="id" type="keyword">fun</span> <span class="id" type="var">x</span> ⇒ <span class="id" type="var">false</span>) [5;9;0] = ([], [5;9;0]).<br/>
<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 

<div class="doc">
<a name="lab122"></a><h2 class="section">映射</h2>

<div class="paragraph"> </div>

 另一个方便的高阶函数叫做 <span class="inlinecode"><span class="id" type="var">map</span></span>。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">map</span> {<span class="id" type="var">X</span> <span class="id" type="var">Y</span>: <span class="id" type="keyword">Type</span>} (<span class="id" type="var">f</span>:<span class="id" type="var">X</span>→<span class="id" type="var">Y</span>) (<span class="id" type="var">l</span>:<span class="id" type="var">list</span> <span class="id" type="var">X</span>) : (<span class="id" type="var">list</span> <span class="id" type="var">Y</span>) :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">l</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;| []     ⇒ []<br/>
&nbsp;&nbsp;| <span class="id" type="var">h</span> :: <span class="id" type="var">t</span> ⇒ (<span class="id" type="var">f</span> <span class="id" type="var">h</span>) :: (<span class="id" type="var">map</span> <span class="id" type="var">f</span> <span class="id" type="var">t</span>)<br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/>
</div>

<div class="doc">
它接受一个函数 <span class="inlinecode"><span class="id" type="var">f</span></span> 和一个列表 <span class="inlinecode"></span> <span class="inlinecode"><span class="id" type="var">l</span></span> <span class="inlinecode">=</span> <span class="inlinecode">[<span class="id" type="var">n<sub>1</sub></span>,</span> <span class="inlinecode"><span class="id" type="var">n<sub>2</sub></span>,</span> <span class="inlinecode"><span class="id" type="var">n<sub>3</sub></span>,</span> <span class="inlinecode">...]</span> <span class="inlinecode"></span>
    并返回列表 <span class="inlinecode"></span> <span class="inlinecode">[<span class="id" type="var">f</span></span> <span class="inlinecode"><span class="id" type="var">n<sub>1</sub></span>,</span> <span class="inlinecode"><span class="id" type="var">f</span></span> <span class="inlinecode"><span class="id" type="var">n<sub>2</sub></span>,</span> <span class="inlinecode"><span class="id" type="var">f</span></span> <span class="inlinecode"><span class="id" type="var">n<sub>3</sub></span>,...]</span> <span class="inlinecode"></span>，其中 <span class="inlinecode"><span class="id" type="var">f</span></span> 可分别应用于 <span class="inlinecode"><span class="id" type="var">l</span></span>
    中的每一个元素。例如： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Example</span> <span class="id" type="var">test_map1</span>: <span class="id" type="var">map</span> (<span class="id" type="keyword">fun</span> <span class="id" type="var">x</span> ⇒ <span class="id" type="var">plus</span> 3 <span class="id" type="var">x</span>) [2;0;2] = [5;3;5].<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
输入列表和输出列表的元素类型不必相同，因为 <span class="inlinecode"><span class="id" type="var">map</span></span> 会接受<b>两个</b>类型参数
    <span class="inlinecode"><span class="id" type="var">X</span></span> 和 <span class="inlinecode"><span class="id" type="var">Y</span></span>，因此它可以应用到一个数值的列表和一个从数值到布尔值的函数，
    并产生一个布尔值列表： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Example</span> <span class="id" type="var">test_map2</span>:<br/>
&nbsp;&nbsp;<span class="id" type="var">map</span> <span class="id" type="var">oddb</span> [2;1;2;5] = [<span class="id" type="var">false</span>;<span class="id" type="var">true</span>;<span class="id" type="var">false</span>;<span class="id" type="var">true</span>].<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
它甚至可以应用到一个数值的列表和一个从数值到布尔值列表的函数，
    并产生一个布尔值的<b>列表的列表</b>： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Example</span> <span class="id" type="var">test_map3</span>:<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">map</span> (<span class="id" type="keyword">fun</span> <span class="id" type="var">n</span> ⇒ [<span class="id" type="var">evenb</span> <span class="id" type="var">n</span>;<span class="id" type="var">oddb</span> <span class="id" type="var">n</span>]) [2;1;2;5]<br/>
&nbsp;&nbsp;= [[<span class="id" type="var">true</span>;<span class="id" type="var">false</span>];[<span class="id" type="var">false</span>;<span class="id" type="var">true</span>];[<span class="id" type="var">true</span>;<span class="id" type="var">false</span>];[<span class="id" type="var">false</span>;<span class="id" type="var">true</span>]].<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a name="lab123"></a><h3 class="section">习题</h3>

<div class="paragraph"> </div>

<a name="lab124"></a><h4 class="section">练习：3 星, standard (map_rev)</h4>
 请证明 <span class="inlinecode"><span class="id" type="var">map</span></span> 和 <span class="inlinecode"><span class="id" type="var">rev</span></span> 可交换。你可能需要定义一个辅助引理 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">map_rev</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">X</span> <span class="id" type="var">Y</span> : <span class="id" type="keyword">Type</span>) (<span class="id" type="var">f</span> : <span class="id" type="var">X</span> → <span class="id" type="var">Y</span>) (<span class="id" type="var">l</span> : <span class="id" type="var">list</span> <span class="id" type="var">X</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">map</span> <span class="id" type="var">f</span> (<span class="id" type="var">rev</span> <span class="id" type="var">l</span>) = <span class="id" type="var">rev</span> (<span class="id" type="var">map</span> <span class="id" type="var">f</span> <span class="id" type="var">l</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab125"></a><h4 class="section">练习：2 星, standard, recommended (flat_map)</h4>
 函数 <span class="inlinecode"><span class="id" type="var">map</span></span> 通过一个类型为 <span class="inlinecode"><span class="id" type="var">X</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">Y</span></span> 的函数将 <span class="inlinecode"><span class="id" type="var">list</span></span> <span class="inlinecode"><span class="id" type="var">X</span></span> 映射到 <span class="inlinecode"><span class="id" type="var">list</span></span> <span class="inlinecode"><span class="id" type="var">Y</span></span>。
    我们可以定义一个类似的函数 <span class="inlinecode"><span class="id" type="var">flat_map</span></span>，它通过一个类型为 <span class="inlinecode"><span class="id" type="var">X</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">list</span></span> <span class="inlinecode"><span class="id" type="var">Y</span></span>
    的函数 <span class="inlinecode"><span class="id" type="var">f</span></span> 将 <span class="inlinecode"><span class="id" type="var">list</span></span> <span class="inlinecode"><span class="id" type="var">X</span></span> 映射到 <span class="inlinecode"><span class="id" type="var">list</span></span> <span class="inlinecode"><span class="id" type="var">Y</span></span>。你的定义应当可以“压扁”<span class="inlinecode"><span class="id" type="var">f</span></span>
    的结果，就像这样：

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">flat_map</span>&nbsp;(<span class="id" type="keyword">fun</span>&nbsp;<span class="id" type="var">n</span>&nbsp;⇒&nbsp;[<span class="id" type="var">n</span>;<span class="id" type="var">n</span>+1;<span class="id" type="var">n</span>+2])&nbsp;[1;5;10]<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;=&nbsp;[1;&nbsp;2;&nbsp;3;&nbsp;5;&nbsp;6;&nbsp;7;&nbsp;10;&nbsp;11;&nbsp;12].
<div class="paragraph"> </div>

</div>

</div>
<div class="code code-tight">

<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">flat_map</span> {<span class="id" type="var">X</span> <span class="id" type="var">Y</span>: <span class="id" type="keyword">Type</span>} (<span class="id" type="var">f</span>: <span class="id" type="var">X</span> → <span class="id" type="var">list</span> <span class="id" type="var">Y</span>) (<span class="id" type="var">l</span>: <span class="id" type="var">list</span> <span class="id" type="var">X</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;: (<span class="id" type="var">list</span> <span class="id" type="var">Y</span>)<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;将本行替换成&nbsp;":=&nbsp;_你的_定义_&nbsp;."&nbsp;*)</span>. <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_flat_map1</span>:<br/>
&nbsp;&nbsp;<span class="id" type="var">flat_map</span> (<span class="id" type="keyword">fun</span> <span class="id" type="var">n</span> ⇒ [<span class="id" type="var">n</span>;<span class="id" type="var">n</span>;<span class="id" type="var">n</span>]) [1;5;4]<br/>
&nbsp;&nbsp;= [1; 1; 1; 5; 5; 5; 4; 4; 4].<br/>
&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 Lists are not the only inductive type for which <span class="inlinecode"><span class="id" type="var">map</span></span> makes sense.
    Here is a <span class="inlinecode"><span class="id" type="var">map</span></span> for the <span class="inlinecode"><span class="id" type="var">option</span></span> type: 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">option_map</span> {<span class="id" type="var">X</span> <span class="id" type="var">Y</span> : <span class="id" type="keyword">Type</span>} (<span class="id" type="var">f</span> : <span class="id" type="var">X</span> → <span class="id" type="var">Y</span>) (<span class="id" type="var">xo</span> : <span class="id" type="var">option</span> <span class="id" type="var">X</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;: <span class="id" type="var">option</span> <span class="id" type="var">Y</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">xo</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">None</span> ⇒ <span class="id" type="var">None</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">Some</span> <span class="id" type="var">x</span> ⇒ <span class="id" type="var">Some</span> (<span class="id" type="var">f</span> <span class="id" type="var">x</span>)<br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/>
</div>

<div class="doc">
<a name="lab126"></a><h4 class="section">练习：2 星, standard, optional (implicit_args)</h4>
 <span class="inlinecode"><span class="id" type="var">filter</span></span> 和 <span class="inlinecode"><span class="id" type="var">map</span></span> 的定义和应用在很多地方使用了隐式参数。
    请将隐式参数外层的花括号替换为圆括号，然后在必要的地方补充显式类型形参并用
    Coq 检查你做的是否正确。（本练习并不会打分，你可以在本文件的<b>副本</b>中做它，
    之后丢掉即可。）
 <span class="proofbox">&#9744;</span> 
</div>

<div class="doc">
<a name="lab127"></a><h2 class="section">折叠</h2>

<div class="paragraph"> </div>

 一个更加强大的高阶函数叫做 <span class="inlinecode"><span class="id" type="var">fold</span></span>。本函数启发自“<span class="inlinecode"><span class="id" type="var">reduce</span></span> 归约”
    操作，它是 Google 的 map/reduce 分布式编程框架的核心。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">fold</span> {<span class="id" type="var">X</span> <span class="id" type="var">Y</span>: <span class="id" type="keyword">Type</span>} (<span class="id" type="var">f</span>: <span class="id" type="var">X</span>→<span class="id" type="var">Y</span>→<span class="id" type="var">Y</span>) (<span class="id" type="var">l</span>: <span class="id" type="var">list</span> <span class="id" type="var">X</span>) (<span class="id" type="var">b</span>: <span class="id" type="var">Y</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;: <span class="id" type="var">Y</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">l</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">nil</span> ⇒ <span class="id" type="var">b</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">h</span> :: <span class="id" type="var">t</span> ⇒ <span class="id" type="var">f</span> <span class="id" type="var">h</span> (<span class="id" type="var">fold</span> <span class="id" type="var">f</span> <span class="id" type="var">t</span> <span class="id" type="var">b</span>)<br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/>
</div>

<div class="doc">
直观上来说，<span class="inlinecode"><span class="id" type="var">fold</span></span> 操作的行为就是将给定的二元操作符 <span class="inlinecode"><span class="id" type="var">f</span></span>
    插入到给定列表的每一对元素之间。例如，<span class="inlinecode"></span> <span class="inlinecode"><span class="id" type="var">fold</span></span> <span class="inlinecode"><span class="id" type="var">plus</span></span> <span class="inlinecode">[1;2;3;4]</span> <span class="inlinecode"></span>
    直观上的意思是 <span class="inlinecode">1+2+3+4</span>。为了让它更精确，我们还需要一个“起始元素”
    作为 <span class="inlinecode"><span class="id" type="var">f</span></span> 初始的第二个输入。因此，例如

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">fold</span>&nbsp;<span class="id" type="var">plus</span>&nbsp;[1;2;3;4]&nbsp;0
<div class="paragraph"> </div>

</div>
    就会产生

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;1&nbsp;+&nbsp;(2&nbsp;+&nbsp;(3&nbsp;+&nbsp;(4&nbsp;+&nbsp;0))).
<div class="paragraph"> </div>

</div>
    以下是更多例子： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Check</span> (<span class="id" type="var">fold</span> <span class="id" type="var">andb</span>).<br/>
<span class="comment">(*&nbsp;===&gt;&nbsp;fold&nbsp;andb&nbsp;:&nbsp;list&nbsp;bool&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;bool&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;bool&nbsp;*)</span><br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">fold_example1</span> :<br/>
&nbsp;&nbsp;<span class="id" type="var">fold</span> <span class="id" type="var">mult</span> [1;2;3;4] 1 = 24.<br/>
<div class="togglescript" id="proofcontrol4" onclick="toggleDisplay('proof4');toggleDisplay('proofcontrol4')"><span class="show"></span></div>
<div class="proofscript" id="proof4" onclick="toggleDisplay('proof4');toggleDisplay('proofcontrol4')">
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">fold_example2</span> :<br/>
&nbsp;&nbsp;<span class="id" type="var">fold</span> <span class="id" type="var">andb</span> [<span class="id" type="var">true</span>;<span class="id" type="var">true</span>;<span class="id" type="var">false</span>;<span class="id" type="var">true</span>] <span class="id" type="var">true</span> = <span class="id" type="var">false</span>.<br/>
<div class="togglescript" id="proofcontrol5" onclick="toggleDisplay('proof5');toggleDisplay('proofcontrol5')"><span class="show"></span></div>
<div class="proofscript" id="proof5" onclick="toggleDisplay('proof5');toggleDisplay('proofcontrol5')">
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">fold_example3</span> :<br/>
&nbsp;&nbsp;<span class="id" type="var">fold</span> <span class="id" type="var">app</span>  [[1];[];[2;3];[4]] [] = [1;2;3;4].<br/>
<div class="togglescript" id="proofcontrol6" onclick="toggleDisplay('proof6');toggleDisplay('proofcontrol6')"><span class="show"></span></div>
<div class="proofscript" id="proof6" onclick="toggleDisplay('proof6');toggleDisplay('proofcontrol6')">
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
<a name="lab128"></a><h4 class="section">练习：1 星, advanced (fold_types_different)</h4>
 我们观察到 <span class="inlinecode"><span class="id" type="var">fold</span></span> 由 <span class="inlinecode"><span class="id" type="var">X</span></span> 和 <span class="inlinecode"><span class="id" type="var">Y</span></span> 这<b>两个</b>类型变量参数化，形参 <span class="inlinecode"><span class="id" type="var">f</span></span>
    则是个接受 <span class="inlinecode"><span class="id" type="var">X</span></span> 和 <span class="inlinecode"><span class="id" type="var">Y</span></span> 并返回 <span class="inlinecode"><span class="id" type="var">Y</span></span> 的二元操作符。你能想出一种 <span class="inlinecode"><span class="id" type="var">X</span></span> 和
    <span class="inlinecode"><span class="id" type="var">Y</span></span> 不同时的应用情景吗？ 
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;请勿修改下面这一行：&nbsp;*)</span><br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">manual_grade_for_fold_types_different</span> : <span class="id" type="var">option</span> (<span class="id" type="var">nat</span>*<span class="id" type="var">string</span>) := <span class="id" type="var">None</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 

<div class="doc">
<a name="lab129"></a><h2 class="section">用函数构造函数</h2>

<div class="paragraph"> </div>

 目前我们讨论过的大部分高阶函数都是接受函数作为参数的。
    现在我们来看一些将函数作为其它函数的结果<b>返回</b>的例子。
    首先，下面是一个接受值 <span class="inlinecode"><span class="id" type="var">x</span></span>（由某个类型 <span class="inlinecode"><span class="id" type="var">X</span></span> 刻画）并返回一个从
    <span class="inlinecode"><span class="id" type="var">nat</span></span> 到 <span class="inlinecode"><span class="id" type="var">X</span></span> 的函数，当它被调用时总是产生 <span class="inlinecode"><span class="id" type="var">x</span></span> 并忽略其 <span class="inlinecode"><span class="id" type="var">nat</span></span> 参数。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">constfun</span> {<span class="id" type="var">X</span>: <span class="id" type="keyword">Type</span>} (<span class="id" type="var">x</span>: <span class="id" type="var">X</span>) : <span class="id" type="var">nat</span>→<span class="id" type="var">X</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">fun</span> (<span class="id" type="var">k</span>:<span class="id" type="var">nat</span>) ⇒ <span class="id" type="var">x</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">ftrue</span> := <span class="id" type="var">constfun</span> <span class="id" type="var">true</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">constfun_example1</span> : <span class="id" type="var">ftrue</span> 0 = <span class="id" type="var">true</span>.<br/>
<div class="togglescript" id="proofcontrol7" onclick="toggleDisplay('proof7');toggleDisplay('proofcontrol7')"><span class="show"></span></div>
<div class="proofscript" id="proof7" onclick="toggleDisplay('proof7');toggleDisplay('proofcontrol7')">
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">constfun_example2</span> : (<span class="id" type="var">constfun</span> 5) 99 = 5.<br/>
<div class="togglescript" id="proofcontrol8" onclick="toggleDisplay('proof8');toggleDisplay('proofcontrol8')"><span class="show"></span></div>
<div class="proofscript" id="proof8" onclick="toggleDisplay('proof8');toggleDisplay('proofcontrol8')">
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
实际上，我们已经见过的多参函数也是讲函数作为数据传入的例子。
    为了理解为什么，请回想 <span class="inlinecode"><span class="id" type="var">plus</span></span> 的类型。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Check</span> <span class="id" type="var">plus</span>.<br/>
<span class="comment">(*&nbsp;==&gt;&nbsp;nat&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;nat&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;nat&nbsp;*)</span><br/>
</div>

<div class="doc">
该表达式中的每个 <span class="inlinecode">→</span> 实际上都是一个类型上的<b>二元</b>操作符。
    该操作符是<b>右结合</b>的，因此 <span class="inlinecode"><span class="id" type="var">plus</span></span> 的类型其实是 <span class="inlinecode"><span class="id" type="var">nat</span></span> <span class="inlinecode">→</span> <span class="inlinecode">(<span class="id" type="var">nat</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">nat</span>)</span>
    的简写，即，它可以读作“<span class="inlinecode"><span class="id" type="var">plus</span></span> 是一个单参数函数，它接受一个 <span class="inlinecode"><span class="id" type="var">nat</span></span>
    并返回另一个函数，该函数接受另一个 <span class="inlinecode"><span class="id" type="var">nat</span></span> 并返回一个 <span class="inlinecode"><span class="id" type="var">nat</span></span>”。
    在上面的例子中，我们总是将 <span class="inlinecode"><span class="id" type="var">plus</span></span> 一次同时应用到两个参数上。
    不过如果我们喜欢，也可以一次只提供一个参数，这叫做<b>偏应用（Partial
    Application）</b>。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">plus3</span> := <span class="id" type="var">plus</span> 3.<br/>
<span class="id" type="keyword">Check</span> <span class="id" type="var">plus3</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_plus3</span> :    <span class="id" type="var">plus3</span> 4 = 7.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_plus3'</span> :   <span class="id" type="var">doit3times</span> <span class="id" type="var">plus3</span> 0 = 9.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_plus3''</span> :  <span class="id" type="var">doit3times</span> (<span class="id" type="var">plus</span> 3) 0 = 9.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a name="lab130"></a><h1 class="section">附加练习</h1>

</div>
<div class="code code-space">

<br/>
<span class="id" type="keyword">Module</span> <span class="id" type="var">Exercises</span>.<br/>
</div>

<div class="doc">
<a name="lab131"></a><h4 class="section">练习：2 星, standard (fold_length)</h4>
 列表的很多通用函数都可以通过 <span class="inlinecode"><span class="id" type="var">fold</span></span> 来实现。例如，下面是
    <span class="inlinecode"><span class="id" type="var">length</span></span> 的另一种实现： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">fold_length</span> {<span class="id" type="var">X</span> : <span class="id" type="keyword">Type</span>} (<span class="id" type="var">l</span> : <span class="id" type="var">list</span> <span class="id" type="var">X</span>) : <span class="id" type="var">nat</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="var">fold</span> (<span class="id" type="keyword">fun</span> <span class="id" type="var">_</span> <span class="id" type="var">n</span> ⇒ <span class="id" type="var">S</span> <span class="id" type="var">n</span>) <span class="id" type="var">l</span> 0.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_fold_length1</span> : <span class="id" type="var">fold_length</span> [4;7;0] = 3.<br/>
<div class="togglescript" id="proofcontrol9" onclick="toggleDisplay('proof9');toggleDisplay('proofcontrol9')"><span class="show"></span></div>
<div class="proofscript" id="proof9" onclick="toggleDisplay('proof9');toggleDisplay('proofcontrol9')">
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
请证明 <span class="inlinecode"><span class="id" type="var">fold_length</span></span> 的正确性。（提示：知道 <span class="inlinecode"><span class="id" type="tactic">reflexivity</span></span> 的化简力度比 <span class="inlinecode"><span class="id" type="tactic">simpl</span></span>
    更大或许会有所帮助。也就是说，你或许会遇到 <span class="inlinecode"><span class="id" type="tactic">simpl</span></span> 无法解决但 <span class="inlinecode"><span class="id" type="tactic">reflexivity</span></span>
    可以解决的目标。） 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">fold_length_correct</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">X</span> (<span class="id" type="var">l</span> : <span class="id" type="var">list</span> <span class="id" type="var">X</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">fold_length</span> <span class="id" type="var">l</span> = <span class="id" type="var">length</span> <span class="id" type="var">l</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab132"></a><h4 class="section">练习：3 星, standard (fold_map)</h4>
 我们也可以用 <span class="inlinecode"><span class="id" type="var">fold</span></span> 来定义 <span class="inlinecode"><span class="id" type="var">map</span></span>。请完成下面的 <span class="inlinecode"><span class="id" type="var">fold_map</span></span>。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">fold_map</span> {<span class="id" type="var">X</span> <span class="id" type="var">Y</span>: <span class="id" type="keyword">Type</span>} (<span class="id" type="var">f</span>: <span class="id" type="var">X</span> → <span class="id" type="var">Y</span>) (<span class="id" type="var">l</span>: <span class="id" type="var">list</span> <span class="id" type="var">X</span>) : <span class="id" type="var">list</span> <span class="id" type="var">Y</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;将本行替换成&nbsp;":=&nbsp;_你的_定义_&nbsp;."&nbsp;*)</span>. <span class="id" type="var">Admitted</span>.<br/>
</div>

<div class="doc">
在 Coq 中写出 <span class="inlinecode"><span class="id" type="var">fold_map_correct</span></span> 来陈述 <span class="inlinecode"><span class="id" type="var">fold_map</span></span> 是正确的，然后证明它。
    （提示：再次提醒，<span class="inlinecode"><span class="id" type="tactic">reflexivity</span></span> 的化简力度比 <span class="inlinecode"><span class="id" type="tactic">simpl</span></span> 更强。） 
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;请勿修改下面这一行：&nbsp;*)</span><br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">manual_grade_for_fold_map</span> : <span class="id" type="var">option</span> (<span class="id" type="var">nat</span>*<span class="id" type="var">string</span>) := <span class="id" type="var">None</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab133"></a><h4 class="section">练习：2 星, advanced (currying)</h4>
 在 Coq 中，函数 <span class="inlinecode"><span class="id" type="var">f</span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" type="var">A</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">B</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">C</span></span> 的类型其实是 <span class="inlinecode"><span class="id" type="var">A</span></span> <span class="inlinecode">→</span> <span class="inlinecode">(<span class="id" type="var">B</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">C</span>)</span>。
    也就是说，如果给 <span class="inlinecode"><span class="id" type="var">f</span></span> 一个类型为 <span class="inlinecode"><span class="id" type="var">A</span></span> 的值，它就会给你函数 <span class="inlinecode"><span class="id" type="var">f'</span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" type="var">B</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">C</span></span>。
    如果再给 <span class="inlinecode"><span class="id" type="var">f'</span></span> 一个类型为 <span class="inlinecode"><span class="id" type="var">B</span></span> 的值，它就会返回一个类型为 <span class="inlinecode"><span class="id" type="var">C</span></span> 的值。
    这为我们提供了 <span class="inlinecode"><span class="id" type="var">plus3</span></span> 中的那种偏应用能力。
    用返回函数的函数处理参数列表的方式被称为<b>柯里化（Currying）</b>，
    它是为了纪念逻辑学家 Haskell Curry。

<div class="paragraph"> </div>

    反正，我们也可以将 <span class="inlinecode"><span class="id" type="var">A</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">B</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">C</span></span> 解释为 <span class="inlinecode">(<span class="id" type="var">A</span></span> <span class="inlinecode">*</span> <span class="inlinecode"><span class="id" type="var">B</span>)</span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">C</span></span>。这叫做
    <b>反柯里化（Uncurrying）</b>。对于反柯里化的二元函数，
    两个参数必须作为序对一次给出，此时它不会偏应用。 
<div class="paragraph"> </div>

 我们可以将柯里化定义如下： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">prod_curry</span> {<span class="id" type="var">X</span> <span class="id" type="var">Y</span> <span class="id" type="var">Z</span> : <span class="id" type="keyword">Type</span>}<br/>
&nbsp;&nbsp;(<span class="id" type="var">f</span> : <span class="id" type="var">X</span> * <span class="id" type="var">Y</span> → <span class="id" type="var">Z</span>) (<span class="id" type="var">x</span> : <span class="id" type="var">X</span>) (<span class="id" type="var">y</span> : <span class="id" type="var">Y</span>) : <span class="id" type="var">Z</span> := <span class="id" type="var">f</span> (<span class="id" type="var">x</span>, <span class="id" type="var">y</span>).<br/>
</div>

<div class="doc">
作为练习，请定义它的反函数 <span class="inlinecode"><span class="id" type="var">prod_uncurry</span></span>，
    然后在下面证明它们互为反函数的定理。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">prod_uncurry</span> {<span class="id" type="var">X</span> <span class="id" type="var">Y</span> <span class="id" type="var">Z</span> : <span class="id" type="keyword">Type</span>}<br/>
&nbsp;&nbsp;(<span class="id" type="var">f</span> : <span class="id" type="var">X</span> → <span class="id" type="var">Y</span> → <span class="id" type="var">Z</span>) (<span class="id" type="var">p</span> : <span class="id" type="var">X</span> * <span class="id" type="var">Y</span>) : <span class="id" type="var">Z</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;将本行替换成&nbsp;":=&nbsp;_你的_定义_&nbsp;."&nbsp;*)</span>. <span class="id" type="var">Admitted</span>.<br/>
</div>

<div class="doc">
举一个柯里化用途的（平凡的）例子，我们可以用它来缩短之前看到的一个例子： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Example</span> <span class="id" type="var">test_map1'</span>: <span class="id" type="var">map</span> (<span class="id" type="var">plus</span> 3) [2;0;2] = [5;3;5].<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
思考练习：在运行以下指令之前，你能计算出 <span class="inlinecode"><span class="id" type="var">prod_curry</span></span> 和 <span class="inlinecode"><span class="id" type="var">prod_uncurry</span></span> 的类型吗？ 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Check</span> @<span class="id" type="var">prod_curry</span>.<br/>
<span class="id" type="keyword">Check</span> @<span class="id" type="var">prod_uncurry</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">uncurry_curry</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">X</span> <span class="id" type="var">Y</span> <span class="id" type="var">Z</span> : <span class="id" type="keyword">Type</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">f</span> : <span class="id" type="var">X</span> → <span class="id" type="var">Y</span> → <span class="id" type="var">Z</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">x</span> <span class="id" type="var">y</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">prod_curry</span> (<span class="id" type="var">prod_uncurry</span> <span class="id" type="var">f</span>) <span class="id" type="var">x</span> <span class="id" type="var">y</span> = <span class="id" type="var">f</span> <span class="id" type="var">x</span> <span class="id" type="var">y</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">curry_uncurry</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">X</span> <span class="id" type="var">Y</span> <span class="id" type="var">Z</span> : <span class="id" type="keyword">Type</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">f</span> : (<span class="id" type="var">X</span> * <span class="id" type="var">Y</span>) → <span class="id" type="var">Z</span>) (<span class="id" type="var">p</span> : <span class="id" type="var">X</span> * <span class="id" type="var">Y</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">prod_uncurry</span> (<span class="id" type="var">prod_curry</span> <span class="id" type="var">f</span>) <span class="id" type="var">p</span> = <span class="id" type="var">f</span> <span class="id" type="var">p</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab134"></a><h4 class="section">练习：2 星, advanced (nth_error_informal)</h4>
 回想 <span class="inlinecode"><span class="id" type="var">nth_error</span></span> 函数的定义：

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">Fixpoint</span>&nbsp;<span class="id" type="var">nth_error</span>&nbsp;{<span class="id" type="var">X</span>&nbsp;:&nbsp;<span class="id" type="keyword">Type</span>}&nbsp;(<span class="id" type="var">l</span>&nbsp;:&nbsp;<span class="id" type="var">list</span>&nbsp;<span class="id" type="var">X</span>)&nbsp;(<span class="id" type="var">n</span>&nbsp;:&nbsp;<span class="id" type="var">nat</span>)&nbsp;:&nbsp;<span class="id" type="var">option</span>&nbsp;<span class="id" type="var">X</span>&nbsp;:=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">match</span>&nbsp;<span class="id" type="var">l</span>&nbsp;<span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;[]&nbsp;⇒&nbsp;<span class="id" type="var">None</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;<span class="id" type="var">a</span>&nbsp;::&nbsp;<span class="id" type="var">l'</span>&nbsp;⇒&nbsp;<span class="id" type="keyword">if</span>&nbsp;<span class="id" type="var">n</span>&nbsp;=?&nbsp;<span class="id" type="var">O</span>&nbsp;<span class="id" type="keyword">then</span>&nbsp;<span class="id" type="var">Some</span>&nbsp;<span class="id" type="var">a</span>&nbsp;<span class="id" type="keyword">else</span>&nbsp;<span class="id" type="var">nth_error</span>&nbsp;<span class="id" type="var">l'</span>&nbsp;(<span class="id" type="var">pred</span>&nbsp;<span class="id" type="var">n</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">end</span>.
<div class="paragraph"> </div>

</div>
   请写出以下定理的非形式化证明：

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span><span class="id" type="var">X</span>&nbsp;<span class="id" type="var">n</span>&nbsp;<span class="id" type="var">l</span>,&nbsp;<span class="id" type="var">length</span>&nbsp;<span class="id" type="var">l</span>&nbsp;=&nbsp;<span class="id" type="var">n</span>&nbsp;→&nbsp;@<span class="id" type="var">nth_error</span>&nbsp;<span class="id" type="var">X</span>&nbsp;<span class="id" type="var">l</span>&nbsp;<span class="id" type="var">n</span>&nbsp;=&nbsp;<span class="id" type="var">None</span>
<div class="paragraph"> </div>

</div>

</div>
<div class="code code-tight">
<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;请勿修改下面这一行：&nbsp;*)</span><br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">manual_grade_for_informal_proof</span> : <span class="id" type="var">option</span> (<span class="id" type="var">nat</span>*<span class="id" type="var">string</span>) := <span class="id" type="var">None</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 The following exercises explore an alternative way of defining
    natural numbers, using the so-called _Church numerals_, named
    after mathematician Alonzo Church.  We can represent a natural
    number <span class="inlinecode"><span class="id" type="var">n</span></span> as a function that takes a function <span class="inlinecode"><span class="id" type="var">f</span></span> as a parameter
    and returns <span class="inlinecode"><span class="id" type="var">f</span></span> iterated <span class="inlinecode"><span class="id" type="var">n</span></span> times. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Module</span> <span class="id" type="var">Church</span>.<br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">cnat</span> := <span style='font-size:120%;'>&forall;</span><span class="id" type="var">X</span> : <span class="id" type="keyword">Type</span>, (<span class="id" type="var">X</span> → <span class="id" type="var">X</span>) → <span class="id" type="var">X</span> → <span class="id" type="var">X</span>.<br/>
</div>

<div class="doc">
我们来看看如何用这种记法写数。将函数迭代一次应当与将它应用一次相同。
    因此： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">one</span> : <span class="id" type="var">cnat</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">fun</span> (<span class="id" type="var">X</span> : <span class="id" type="keyword">Type</span>) (<span class="id" type="var">f</span> : <span class="id" type="var">X</span> → <span class="id" type="var">X</span>) (<span class="id" type="var">x</span> : <span class="id" type="var">X</span>) ⇒ <span class="id" type="var">f</span> <span class="id" type="var">x</span>.<br/>
</div>

<div class="doc">
与此类似，<span class="inlinecode"><span class="id" type="var">two</span></span> 应当对其参数应用两次 <span class="inlinecode"><span class="id" type="var">f</span></span>： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">two</span> : <span class="id" type="var">cnat</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">fun</span> (<span class="id" type="var">X</span> : <span class="id" type="keyword">Type</span>) (<span class="id" type="var">f</span> : <span class="id" type="var">X</span> → <span class="id" type="var">X</span>) (<span class="id" type="var">x</span> : <span class="id" type="var">X</span>) ⇒ <span class="id" type="var">f</span> (<span class="id" type="var">f</span> <span class="id" type="var">x</span>).<br/>
</div>

<div class="doc">
定义 <span class="inlinecode"><span class="id" type="var">zero</span></span> 有点刁钻：我们如何“将函数应用零次”？答案很简单：
    把参数原样返回就好。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">zero</span> : <span class="id" type="var">cnat</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">fun</span> (<span class="id" type="var">X</span> : <span class="id" type="keyword">Type</span>) (<span class="id" type="var">f</span> : <span class="id" type="var">X</span> → <span class="id" type="var">X</span>) (<span class="id" type="var">x</span> : <span class="id" type="var">X</span>) ⇒ <span class="id" type="var">x</span>.<br/>
</div>

<div class="doc">
更一般地说，数 <span class="inlinecode"><span class="id" type="var">n</span></span> 可以写作 <span class="inlinecode"><span class="id" type="keyword">fun</span></span> <span class="inlinecode"><span class="id" type="var">X</span></span> <span class="inlinecode"><span class="id" type="var">f</span></span> <span class="inlinecode"><span class="id" type="var">x</span></span> <span class="inlinecode">⇒</span> <span class="inlinecode"><span class="id" type="var">f</span></span> <span class="inlinecode">(<span class="id" type="var">f</span></span>
    <span class="inlinecode">...</span> <span class="inlinecode">(<span class="id" type="var">f</span></span> <span class="inlinecode"><span class="id" type="var">x</span>)</span> <span class="inlinecode">...)</span>，其中 <span class="inlinecode"><span class="id" type="var">f</span></span> 出现了 <span class="inlinecode"><span class="id" type="var">n</span></span> 次。要特别注意我们之前定义
    <span class="inlinecode"><span class="id" type="var">doit3times</span></span> 函数的方式就是 <span class="inlinecode">3</span> 的邱奇数表示。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">three</span> : <span class="id" type="var">cnat</span> := @<span class="id" type="var">doit3times</span>.<br/>
</div>

<div class="doc">
完成以下函数的定义。请用 <span class="inlinecode"><span class="id" type="tactic">reflexivity</span></span> 证明来确认它们能够通过对应的单元测试。 
<div class="paragraph"> </div>

<a name="lab135"></a><h4 class="section">练习：1 星, advanced (church_succ)</h4>

<div class="paragraph"> </div>

 Successor of a natural number: given a Church numeral <span class="inlinecode"><span class="id" type="var">n</span></span>,
    the successor <span class="inlinecode"><span class="id" type="var">succ</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> is a function that iterates its
    argument once more than <span class="inlinecode"><span class="id" type="var">n</span></span>. 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Definition</span> <span class="id" type="var">succ</span> (<span class="id" type="var">n</span> : <span class="id" type="var">cnat</span>) : <span class="id" type="var">cnat</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;将本行替换成&nbsp;":=&nbsp;_你的_定义_&nbsp;."&nbsp;*)</span>. <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">succ_1</span> : <span class="id" type="var">succ</span> <span class="id" type="var">zero</span> = <span class="id" type="var">one</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">succ_2</span> : <span class="id" type="var">succ</span> <span class="id" type="var">one</span> = <span class="id" type="var">two</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">succ_3</span> : <span class="id" type="var">succ</span> <span class="id" type="var">two</span> = <span class="id" type="var">three</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab136"></a><h4 class="section">练习：1 星, advanced (church_plus)</h4>

<div class="paragraph"> </div>

 Addition of two natural numbers: 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Definition</span> <span class="id" type="var">plus</span> (<span class="id" type="var">n</span> <span class="id" type="var">m</span> : <span class="id" type="var">cnat</span>) : <span class="id" type="var">cnat</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;将本行替换成&nbsp;":=&nbsp;_你的_定义_&nbsp;."&nbsp;*)</span>. <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">plus_1</span> : <span class="id" type="var">plus</span> <span class="id" type="var">zero</span> <span class="id" type="var">one</span> = <span class="id" type="var">one</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">plus_2</span> : <span class="id" type="var">plus</span> <span class="id" type="var">two</span> <span class="id" type="var">three</span> = <span class="id" type="var">plus</span> <span class="id" type="var">three</span> <span class="id" type="var">two</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">plus_3</span> :<br/>
&nbsp;&nbsp;<span class="id" type="var">plus</span> (<span class="id" type="var">plus</span> <span class="id" type="var">two</span> <span class="id" type="var">two</span>) <span class="id" type="var">three</span> = <span class="id" type="var">plus</span> <span class="id" type="var">one</span> (<span class="id" type="var">plus</span> <span class="id" type="var">three</span> <span class="id" type="var">three</span>).<br/>
<span class="id" type="keyword">Proof</span>. <span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab137"></a><h4 class="section">练习：2 星, advanced (church_mult)</h4>

<div class="paragraph"> </div>

 Multiplication: 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Definition</span> <span class="id" type="var">mult</span> (<span class="id" type="var">n</span> <span class="id" type="var">m</span> : <span class="id" type="var">cnat</span>) : <span class="id" type="var">cnat</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;将本行替换成&nbsp;":=&nbsp;_你的_定义_&nbsp;."&nbsp;*)</span>. <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">mult_1</span> : <span class="id" type="var">mult</span> <span class="id" type="var">one</span> <span class="id" type="var">one</span> = <span class="id" type="var">one</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">mult_2</span> : <span class="id" type="var">mult</span> <span class="id" type="var">zero</span> (<span class="id" type="var">plus</span> <span class="id" type="var">three</span> <span class="id" type="var">three</span>) = <span class="id" type="var">zero</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">mult_3</span> : <span class="id" type="var">mult</span> <span class="id" type="var">two</span> <span class="id" type="var">three</span> = <span class="id" type="var">plus</span> <span class="id" type="var">three</span> <span class="id" type="var">three</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab138"></a><h4 class="section">练习：2 星, advanced (church_exp)</h4>

<div class="paragraph"> </div>

 Exponentiation: 
<div class="paragraph"> </div>

 (_Hint_: Polymorphism plays a crucial role here.  However,
    choosing the right type to iterate over can be tricky.  If you hit
    a "Universe inconsistency" error, try iterating over a different
    type.  Iterating over <span class="inlinecode"><span class="id" type="var">cnat</span></span> itself is usually problematic.) 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">exp</span> (<span class="id" type="var">n</span> <span class="id" type="var">m</span> : <span class="id" type="var">cnat</span>) : <span class="id" type="var">cnat</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;将本行替换成&nbsp;":=&nbsp;_你的_定义_&nbsp;."&nbsp;*)</span>. <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">exp_1</span> : <span class="id" type="var">exp</span> <span class="id" type="var">two</span> <span class="id" type="var">two</span> = <span class="id" type="var">plus</span> <span class="id" type="var">two</span> <span class="id" type="var">two</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">exp_2</span> : <span class="id" type="var">exp</span> <span class="id" type="var">three</span> <span class="id" type="var">zero</span> = <span class="id" type="var">one</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">exp_3</span> : <span class="id" type="var">exp</span> <span class="id" type="var">three</span> <span class="id" type="var">two</span> = <span class="id" type="var">plus</span> (<span class="id" type="var">mult</span> <span class="id" type="var">two</span> (<span class="id" type="var">mult</span> <span class="id" type="var">two</span> <span class="id" type="var">two</span>)) <span class="id" type="var">one</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="code code-tight">

<span class="id" type="keyword">End</span> <span class="id" type="var">Church</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">End</span> <span class="id" type="var">Exercises</span>.<br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;Mon&nbsp;Oct&nbsp;28&nbsp;08:14:23&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
</div>
</div>



</div>

</body>
</html>